Upgrade optlib from 4.13 to 4.29

Optlib/Algorithm/ADMM/Inv_bounded.lean

@@ -14,21 +14,21 @@ variable {X Y:Type*}
 [NormedAddCommGroup Y] [InnerProductSpace ℝ Y]
 (A : X →L[ℝ] Y)(fullrank: Injective A)
 
-lemma KerA_bot (fullrank: Injective A): ker A = ⊥ := ker_eq_bot.2 fullrank
+lemma KerA_bot (fullrank: Injective A): A.toLinearMap.ker = ⊥ := LinearMap.ker_eq_bot.2 fullrank
 
 variable [CompleteSpace X] [CompleteSpace Y]
 
-lemma KerA_eq_KerA'A : ker A = ker (A†.comp A) := by
+lemma KerA_eq_KerA'A : A.toLinearMap.ker = (A†.comp A).toLinearMap.ker := by
    ext x; constructor; simp
    ·  intro h; rw[h]; continuity
    ·  intro h; simp at h
-      have : ((inner (A x) (A x)):ℝ) = (0:ℝ) := by
+      have : ((inner ℝ (A x) (A x)):ℝ) = (0:ℝ) := by
          calc
-            _ = (inner x ((A†) (A x)):ℝ) := by rw [ContinuousLinearMap.adjoint_inner_right]
+            _ = (inner ℝ x ((A†) (A x)):ℝ) := by rw [ContinuousLinearMap.adjoint_inner_right]
             _ = (0:ℝ) := by rw [h, inner_zero_right]
       apply inner_self_eq_zero.1 this
 
-lemma KerA'A_bot (fullrank: Injective A) : ker (A†.comp A) = ⊥ := by
+lemma KerA'A_bot (fullrank: Injective A) : (A†.comp A).toLinearMap.ker = ⊥ := by
    rw[← KerA_eq_KerA'A]
    apply KerA_bot A fullrank
 

Optlib/Algorithm/ADMM/Lemma.lean

@@ -61,6 +61,7 @@ local notation "y'" => admm_kkt.y
 local notation "A₁†" => ContinuousLinearMap.adjoint A₁
 local notation "A₂†" => ContinuousLinearMap.adjoint A₂
 local notation "⟪" a₁ ", " a₂ "⟫" => @inner ℝ _ _ a₁ a₂
+local notation "inner" => (inner ℝ)
 
 lemma Satisfaction_ofthekkt : Convex_KKT x₁' x₂' y' admm.toOptProblem := admm_kkt.h
 
@@ -189,7 +190,7 @@ lemma norm_covex1 [Setting E₁ E₂ F admm admm_kkt]:∀ n : ℕ+ ,
    let g := A₁
    have h2 : u ∘ g = f := by
       ext x
-      simp only [Function.comp_apply]
+      rfl
    rw[← h2]
    have h3 : ⇑g ⁻¹' univ = univ := by
       simp only [preimage_univ]
@@ -223,7 +224,7 @@ lemma norm_covex2 [Setting E₁ E₂ F admm admm_kkt]:∀ n : ℕ+ ,
    let g := A₂
    have h2 : u ∘ g = f := by
       ext x
-      simp only [Function.comp_apply]
+      rfl
    rw[← h2]
    have h3 : ⇑g ⁻¹' univ = univ := by
       simp only [preimage_univ]
@@ -280,10 +281,7 @@ lemma ADMM_iter_process₁'_eq3_2' [Setting E₁ E₂ F admm admm_kkt]: ∀ n :
             ((OptProblem.A₂ E₁) (ADMM.x₂ E₁ F n.natPred) - OptProblem.b E₁ E₂)
    rw[this]
    show HasGradientAt ((fun x => ⟪c , (A₁ x)⟫ + c₁)) (A₁† c) x
-   rw[hasGradientAt_iff_hasFDerivAt]
-   apply HasFDerivAt.add_const _ c₁
-   show HasGradientAt ((fun x => ⟪c , (A₁ x)⟫)) (A₁† c) x
-   apply ADMM_iter_process₁'_eq3_2'_1
+   exact (ADMM_iter_process₁'_eq3_2'_1 (c := c) x).add_const c₁
 
 lemma inner_continuous1 [Setting E₁ E₂ F admm admm_kkt]:∀ n : ℕ+ ,
       ContinuousOn (fun x => ⟪y n.natPred , (A₁ x) + (A₂ (x₂ n.natPred)) - b⟫) univ:= by
@@ -325,8 +323,7 @@ lemma Gradient_of_quadratic_forms { α β : Type*}
       simp[h]
       have := norm_nonneg (s - x)
       rwa[mul_nonneg_iff_right_nonneg_of_pos εpos]
-   ·  use ε / ‖A‖ ^ 2
-      field_simp
+   ·  refine ⟨ε / ‖A‖ ^ 2, div_pos εpos (sq_pos_of_pos h), ?_⟩
       intro x hx
       have hzero : 0 < ‖A‖ ^ 2 := by apply sq_pos_of_pos h
       let t := x - s
@@ -343,7 +340,7 @@ lemma Gradient_of_quadratic_forms { α β : Type*}
          rw[real_inner_smul_left,ContinuousLinearMap.adjoint_inner_left]
          ring
       rw[this,real_inner_self_eq_norm_sq]
-      simp only [abs_pow, abs_norm, ge_iff_le]
+      rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
       calc
          _ = ‖A (s - x)‖ ^ 2 := by
             rw[norm_comm]
@@ -367,7 +364,6 @@ lemma Gradient_of_quadratic_forms { α β : Type*}
                apply mul_le_mul_of_nonneg_left hx this
             _ = _ := by
                field_simp[hzero]
-               ring_nf
 
 #check add_sub
 lemma ADMM_iter_process₁'_eq3_3' [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+ ,
@@ -558,10 +554,7 @@ lemma ADMM_iter_process₂'_eq3_2' [Setting E₁ E₂ F admm admm_kkt]: ∀ n :
       exact inner_add_right (y n.natPred) (A₂ x) (A₁ (x₁ n) - b)
    rw[this]
    show HasGradientAt (fun x => ⟪c , (A₂ x)⟫ + c₁) (A₂† c) x
-   rw[hasGradientAt_iff_hasFDerivAt]
-   apply HasFDerivAt.add_const _ c₁
-   show HasGradientAt ((fun x => ⟪c , (A₂ x)⟫)) (A₂† c) x
-   apply inner_gradient
+   exact (inner_gradient (A := A₂) (c := c) x).add_const c₁
 
 lemma inner_continuous2 [Setting E₁ E₂ F admm admm_kkt]:∀ n : ℕ+ ,
       ContinuousOn (fun x => ⟪y n.natPred , (A₁ (x₁ n)) + (A₂ x) - b⟫) univ:= by
@@ -854,7 +847,7 @@ lemma subgradientAt_mono_u [Setting E₁ E₂ F admm admm_kkt] : ∀ n : ℕ+,
       (0 : ℝ) ≤ (inner (u (n) + A₁† y') (x₁ (n) - x₁')) := by
    intro n
    calc
-      _= inner (u (n) - (- A₁† y')) (x₁ (n) - x₁') := by simp[v]
+      _= inner (u (n) - (- A₁† y')) (x₁ (n) - x₁') := by simp
       _≥ (0 : ℝ) := by
          apply subgradientAt_mono
          apply u_inthesubgradient
@@ -864,7 +857,7 @@ lemma subgradientAt_mono_v [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+,
       (0 : ℝ) ≤ (inner (v (n) + A₂† y') (x₂ (n) - x₂')) := by
    intro n
    calc
-      _= inner (v (n) - (- A₂† y')) (x₂ (n) - x₂') := by simp[v]
+      _= inner (v (n) - (- A₂† y')) (x₂ (n) - x₂') := by simp
       _≥ (0 : ℝ) := by
          apply subgradientAt_mono
          apply v_inthesubgradient
@@ -883,7 +876,7 @@ lemma expended_u_gt_zero [Setting E₁ E₂ F admm admm_kkt]: ∀ n, (0 : ℝ) 
    let x_diff := x₁ (n + 1) - x₁'
    let succ_n := Nat.toPNat' (n + 1)
    calc
-      _= inner (𝕜 := ℝ) block Ae1 := by rfl
+      _= inner block Ae1 := by rfl
       _= inner (A₁† block) (e') := by rw [ContinuousLinearMap.adjoint_inner_left]
       _= inner (u' + A₁† y') (x_diff) := by
          let block₁ := y (n + 1) + ((1-τ) * ρ) • (A₁ (e₁ (n + 1)) + A₂ (e₂ (n + 1))) + (ρ • (A₂ (x₂ (n) - x₂ (n+1))))
@@ -954,7 +947,7 @@ lemma expended_u_v_gt_zero [Setting E₁ E₂ F admm admm_kkt]: ∀ n , (inner (
    let Ae2 := A₂ (e₂ (n + 1))
    calc
    _ = inner ey' (-(A_e_sum)) - (1 - τ) * ρ * (inner A_e_sum A_e_sum)
-      + ρ * (inner (A_x_sum) (Ae1)) := by rw [norm_sq_eq_inner (𝕜:=ℝ) (A_e_sum)];rfl
+      + ρ * (inner (A_x_sum) (Ae1)) := by rw [← real_inner_self_eq_norm_sq A_e_sum]
    _ = inner ey' (-(A_e_sum)) + inner (- ((1 - τ) * ρ) • A_e_sum) A_e_sum
       + ρ * (inner A_x_sum Ae1) := by rw [smul_left,starRingEnd_eq_R];ring
    _ = inner (-ey') A_e_sum + inner (- ((1 - τ) * ρ) • A_e_sum) A_e_sum
@@ -1244,7 +1237,7 @@ lemma Φ_isdescending_inequ5' [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+,
       - 2 * (1-τ) * ρ * ‖A₁ (x₁ (n+1)) + A₂ (x₂ (n+1)) - b‖^2
       + 2 * M (n+1)
       - 1 * ρ * ((‖A₂ (x₂ (n+1) - x₂ n)‖^2 + ‖A₂ (e₂ (n+1))‖^2 - ‖A₂ (e₂ n)‖^2))
-      := by nth_rw 2 [div_eq_mul_inv]; rw [one_mul]; nth_rw 3 [pow_two]; simp [inv_mul_cancel]
+      := by nth_rw 2 [div_eq_mul_inv]; rw [one_mul]; nth_rw 3 [pow_two]; simp
             left; rw [mul_assoc]
             nth_rw 2 [← mul_assoc]
             nth_rw 2 [← mul_assoc]
@@ -1399,7 +1392,11 @@ lemma basic_inequ₂ (n : ℕ+) : - 2 * inner (A₂ (x₂ (n+1) - x₂ n)) (A₁
       apply Real.sqrt_ne_zero'.mpr
       rcases admm.htau with ⟨h₁, _⟩
       assumption
-   have h3 : inner (𝕜 := ℝ) S1 S2 = inner (𝕜 := ℝ) (s1 • S1) (s1⁻¹ • S2) := by rw [inner_smul_left, inner_smul_right]; rw [← mul_assoc]; simp; rw [mul_inv_cancel₀, one_mul]; exact this
+   have h3 : inner S1 S2 = inner (s1 • S1) (s1⁻¹ • S2) := by
+      rw [inner_smul_left, inner_smul_right, ← mul_assoc]
+      simp
+      rw [mul_inv_cancel₀, one_mul]
+      exact this
    rw [h1, h2, h3]
    have : ‖s1 • S1‖ ^ 2 + ‖s1⁻¹ • S2‖ ^ 2 - -2 * ⟪s1 • S1, s1⁻¹ • S2⟫_ℝ = ‖s1 • S1‖ ^ 2 + 2 * ⟪s1 • S1, s1⁻¹ • S2⟫_ℝ + ‖s1⁻¹ • S2‖ ^ 2 := by ring_nf
    rw [this, ←norm_add_sq_real]
@@ -1478,13 +1475,20 @@ lemma τ_min1_1 [Setting E₁ E₂ F admm admm_kkt] (h: 0 < τ ∧ τ ≤ 1) : m
    rcases h with ⟨h1, h2⟩
    apply min_eq_left
    have h3: τ ^ 2 ≤ 1 := by
-      apply pow_le_one;linarith;linarith
+      have hτ : |τ| ≤ 1 := by simpa [abs_of_nonneg (le_of_lt h1)] using h2
+      have hτ' : |τ| ≤ |(1 : ℝ)| := by simpa using hτ
+      have hsq : τ ^ 2 ≤ (1 : ℝ) ^ 2 := (sq_le_sq).2 hτ'
+      simpa using hsq
    linarith
 
 lemma τ_min1_2 [Setting E₁ E₂ F admm admm_kkt] (h: τ > 1 ) : min τ (1 + τ - τ ^ 2) = 1 + τ - τ ^ 2 := by
    apply min_eq_right
    have : 1 < τ ^ 2 := by
-      apply one_lt_pow;exact h;linarith
+      have hτ : 0 < τ := lt_trans zero_lt_one h
+      have hτabs : (1 : ℝ) < |τ| := by simpa [abs_of_pos hτ] using h
+      have hτabs' : |(1 : ℝ)| < |τ| := by simpa using hτabs
+      have hsq : (1 : ℝ) ^ 2 < τ ^ 2 := (sq_lt_sq).2 hτabs'
+      simpa using hsq
    linarith
 
 lemma τ_min2_1 [Setting E₁ E₂ F admm admm_kkt] (h: 0 < τ ∧ τ ≤ 1) : min 1 (1 + 1 / τ - τ ) = 1 := by
@@ -1503,7 +1507,9 @@ lemma τ_min2_2 [Setting E₁ E₂ F admm admm_kkt] (h: τ > 1 ) : min 1 (1 + 1
    calc
       _ > 1 := h
       _ > 1 / τ := by
-         rw [one_div, ← inv_one];apply inv_lt_inv_of_lt;linarith;exact h
+         have hτ : 0 < τ := lt_trans zero_lt_one h
+         have hdiv1 : 1 / τ < 1 := (div_lt_iff₀ hτ).2 (by simpa [one_mul] using h)
+         linarith [hdiv1]
    linarith
 
 lemma τ_min3_1 [Setting E₁ E₂ F admm admm_kkt] (h: 0 < τ ∧ τ ≤ 1) : max (1 - τ) (1 - 1 / τ) = 1 - τ := by
@@ -1522,7 +1528,9 @@ lemma τ_min3_2 [Setting E₁ E₂ F admm admm_kkt] (h: τ > 1) : max (1 - τ) (
    calc
       _ > 1 := h
       _ > 1 / τ := by
-         rw [one_div, ← inv_one];apply inv_lt_inv_of_lt;linarith;exact h
+         have hτ : 0 < τ := lt_trans zero_lt_one h
+         have hdiv1 : 1 / τ < 1 := (div_lt_iff₀ hτ).2 (by simpa [one_mul] using h)
+         linarith [hdiv1]
    linarith
 
 lemma Φ_isdescending [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+, (Φ n ) - (Φ (n + 1) ) ≥ (min τ (1 + τ - τ ^ 2) )* ρ

Optlib/Algorithm/ADMM/Scheme.lean

@@ -35,7 +35,7 @@ def Admm_sub_Isunique {E : Type*}(f : E → ℝ)(x : E)(_h : IsMinOn f univ x):
 -- Augmented Lagrangian Function
 def Augmented_Lagrangian_Function (opt : OptProblem E₁ E₂ F) (ρ : ℝ) : E₁ × E₂ × F → ℝ :=
    fun (x₁ , x₂ , y) => (opt.f₁ x₁) + (opt.f₂ x₂) +
-      inner y  ((opt.A₁ x₁) + (opt.A₂ x₂) - opt.b) + ρ / 2 * ‖(opt.A₁ x₁) + (opt.A₂ x₂) - opt.b‖ ^ 2
+      inner ℝ y ((opt.A₁ x₁) + (opt.A₂ x₂) - opt.b) + ρ / 2 * ‖(opt.A₁ x₁) + (opt.A₂ x₂) - opt.b‖ ^ 2
 
 -- The basic iteration format of ADMM
 class ADMM extends (OptProblem E₁ E₂ F) where

Optlib/Algorithm/ADMM/Theroem_converge.lean

@@ -88,9 +88,9 @@ lemma nonneg₁ [Setting E₁ E₂ F admm admm_kkt]: min τ (1 + τ - τ ^ 2) >
 lemma nonneg₂ [Setting E₁ E₂ F admm admm_kkt]: min 1 (1 + 1 / τ - τ) > 0 := by
    rcases admm.htau with ⟨h1, _⟩
    have h2: 1 + 1/τ - τ > 0 := by
-      field_simp;rw [← sq]
-      have h3 : 1 + τ - τ ^ 2 > 0 := nonneg_prime
-      linarith
+      have hτ : τ ≠ 0 := ne_of_gt h1
+      rw [show 1 + 1 / τ - τ = (1 + τ - τ ^ 2) / τ by field_simp [hτ]; ring]
+      exact div_pos nonneg_prime h1
    apply lt_min one_pos h2
 
 lemma Φ₁_nonneg [Setting E₁ E₂ F admm admm_kkt]:
@@ -165,21 +165,23 @@ lemma Φ_is_nonneg [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ , Φ n ≥ 0
 
 lemma Φ_bd_above [Setting E₁ E₂ F admm admm_kkt]: ∃ C : ℝ, ∀ n : ℕ, Φ n < C := by
    let C := Max.max ((Φ 0) + 1) ((Φ 1) + 1); use C; intro n
-   induction' n with k h
-   ·  have : Φ 0 < (Φ 0) + 1 := by linarith
+   induction n with
+   | zero =>
+      have : Φ 0 < (Φ 0) + 1 := by linarith
       apply lt_max_iff.2
       left; exact this
-   ·  by_cases hh : k = 0
-      ·  rw [hh,zero_add]
-         apply lt_max_iff.2
-         right; linarith
-      ·  push_neg at hh
-         have k_pos : k > 0 := by apply Nat.pos_of_ne_zero hh
-         have : (Φ) (k.toPNat k_pos) ≥ (Φ) ((k.toPNat k_pos ) + 1) := by
-            apply Φ_is_monotone
-         have h' : Φ (k.toPNat k_pos) < C := by apply h
-         show Φ ((k.toPNat k_pos) + 1) < C
-         linarith
+   | succ k h =>
+      by_cases hh : k = 0
+      · rw [hh,zero_add]
+        apply lt_max_iff.2
+        right; linarith
+      · push_neg at hh
+        have k_pos : k > 0 := by exact Nat.pos_of_ne_zero hh
+        have : (Φ) (k.toPNat k_pos) ≥ (Φ) ((k.toPNat k_pos) + 1) := by
+          apply Φ_is_monotone
+        have h' : Φ (k.toPNat k_pos) < C := by simpa using h
+        show Φ ((k.toPNat k_pos) + 1) < C
+        linarith
 
 lemma Φ_isBounded' [Setting E₁ E₂ F admm admm_kkt] : ∃ (r : ℝ), (range Φ) ⊆ ball 0 r := by
    rcases Φ_bd_above with ⟨C,bd⟩
@@ -317,9 +319,7 @@ lemma A₂e₂_isBounded' [Setting E₁ E₂ F admm admm_kkt]: ∃ (r : ℝ), (r
             exact h3; simp
 
    have h6: dist (A₂ (e₂ n)) 0 < √ (r_Φ / ρ) := by
-      rw[← sub_zero (A₂ (e₂ n))] at h5
-      rw[SeminormedAddGroup.dist_eq (A₂ (e₂ n)) 0]
-      exact h5
+      simpa [dist_eq_norm] using h5
 
    rw [← hr] at h6
    rw [← Metric.mem_ball] at h6
@@ -434,9 +434,7 @@ lemma A₁e₁_A₂e₂_isBounded'[Setting E₁ E₂ F admm admm_kkt] : ∃ (r :
 
    have h6: dist (A₁ (e₁ n) + A₂ (e₂ n)) 0 < r := by
       have h_n' := h_n n
-      rw[← sub_zero (A₁ (e₁ n) + A₂ (e₂ n))] at h_n'
-      rw[SeminormedAddGroup.dist_eq (A₁ (e₁ n) + A₂ (e₂ n)) 0]
-      exact h_n'
+      simpa [dist_eq_norm] using h_n'
 
    rw [← Metric.mem_ball] at h6; simp; simp at h6
    exact h6
@@ -481,9 +479,7 @@ lemma A₁e₁_isBounded' [Setting E₁ E₂ F admm admm_kkt]: ∃ (r : ℝ), ra
          _ = r := hr
 
    have h_dist : dist (A₁ (e₁ n)) 0 < r := by
-      rw[← sub_zero (A₁ (e₁ n))] at h_norm
-      rw[SeminormedAddGroup.dist_eq (A₁ (e₁ n)) 0]
-      exact h_norm
+      simpa [dist_eq_norm] using h_norm
 
    rw [← Metric.mem_ball] at h_dist
    apply h_dist
@@ -679,7 +675,8 @@ lemma Φ_Summable₁' [Setting E₁ E₂ F admm admm_kkt] :
    intro n
    let φ₀ := (fun i : ℕ => Φ i.succ)
    have : ∀ i ∈ Finset.range n , (φ₀ i)-(φ₀ (i+1)) = (Φ i.succ ) - (Φ (i.succ + 1)) := by
-      simp only [Finset.mem_range, Nat.succ_eq_add_one, implies_true]
+      intro i hi
+      rfl
    have h : Finset.range n =Finset.range n := rfl
    rw[← Finset.sum_congr h this , Finset.sum_range_sub']
    simp only [φ₀]
@@ -701,16 +698,7 @@ lemma Φ_isSummable [Setting E₁ E₂ F admm admm_kkt] : Summable (fun n : ℕ
 theorem summable_of_nonneg_of_le {β : Type*} {f : β → ℝ} {g : β → ℝ}
 (hg : ∀ (n : β), 0 ≤ g n) (hgf : ∀ (n : β), g n ≤ f n) (hf : Summable f) :
 Summable g:=by
-  rw[← NNReal.summable_mk]
-  have f_ge_zero :∀ (n : β), 0 ≤ f n := by
-   intro n
-   apply le_trans (hg n) (hgf n)
-  have :∀ (n : β), (⟨g n, hg n⟩ : NNReal) ≤ ⟨f n , f_ge_zero n⟩ := by
-   simp only [Subtype.mk_le_mk]
-   apply hgf
-  apply NNReal.summable_of_le this
-  rw[← NNReal.summable_coe]
-  exact hf
+  exact Summable.of_nonneg_of_le hg hgf hf
 
 lemma Φ_inequ₁ [Setting E₁ E₂ F admm admm_kkt] (m : ℕ+):
       (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (m+1)) + A₂ (e₂ (m+1))‖ ^ 2 ≤ Φ m - Φ (m + 1) := by