import Optlib.Function.Proximal
import Mathlib.Topology.MetricSpace.Sequences
import Optlib.Algorithm.ADMM.Lemma
import Optlib.Algorithm.ADMM.Scheme
import Optlib.Convex.ImageSubgradientClosed

noncomputable section

open Set InnerProductSpace Topology Filter Bornology Metric Real

variable {E₁ E₂ F : Type*}
[NormedAddCommGroup E₁] [InnerProductSpace ℝ E₁] [FiniteDimensional ℝ E₁]
[NormedAddCommGroup E₂] [InnerProductSpace ℝ E₂] [FiniteDimensional ℝ E₂]
[NormedAddCommGroup F ] [InnerProductSpace ℝ F ] [FiniteDimensional ℝ F]

variable(admm : ADMM E₁ E₂ F)

namespace ADMM_Converge_Proof

variable {admm admm_kkt}

local notation "f₁" => admm.f₁
local notation "f₂" => admm.f₂
local notation "A₁" => admm.A₁
local notation "A₂" => admm.A₂
local notation "b" => admm.b
local notation "x₁" => admm.x₁
local notation "x₂" => admm.x₂
local notation "y" => admm.y
local notation "τ" => admm.τ
local notation "ρ" => admm.ρ

local notation "x₁'" => admm_kkt.x₁
local notation "x₂'" => admm_kkt.x₂
local notation "y'" => admm_kkt.y

local notation "A₁†" => ContinuousLinearMap.adjoint A₁
local notation "A₂†" => ContinuousLinearMap.adjoint A₂

section

-- variable [Setting E₁ E₂ F admm admm_kkt]

lemma inSet {X : Type*} ( f : ℕ → X ) : ∀ n : ℕ , f n ∈ range f := by
   intro n;use n

lemma nonneg_prime [Setting E₁ E₂ F admm admm_kkt]: 1 + τ - τ ^ 2 > 0 := by
   rcases admm.htau with ⟨h1, _⟩
   have h0 : 1 + τ - τ ^ 2 = - (τ - 1/2)^ 2 + 5/4 := by ring
   rw [h0];simp only [one_div, gt_iff_lt, lt_neg_add_iff_add_lt, add_zero]
   have h2 : 5/4 = |√5/2|^2:= by
      rw [sq_abs]; field_simp; norm_num
   rw [h2];apply sq_lt_sq.mpr;simp only [abs_abs]
   have h6 : |τ - 2⁻¹| < √5/2 := by
      let θ := τ - 2⁻¹
      have h7 : |θ| < √5/2 := by
         have g1 : (1 + √5) / 2 - 1 / 2 = √5 / 2 := by ring
         have h8 : θ < √5/2 :=
         calc
            _ = τ - 2⁻¹ := by rfl
            _ < (1 + √5) / 2 - 2⁻¹ := by linarith [h2]
            _ = √5/2 := by norm_num [g1]
         have h9 : -(√5/2) < θ := by
            have g2 : 1/2 < √5/2 := by
               apply div_lt_div_of_pos_right _ zero_lt_two
               apply (lt_sqrt _).mpr _
               repeat norm_num
            have h10 : θ > -(√5/2) := by
               calc
                  _ = τ - 2⁻¹ := by rfl
                  _ > 0 - 2⁻¹ := by linarith [h1]
                  _ > -(√5/2) := by norm_num [g2]
            rwa[← gt_iff_lt]
         rw[abs_lt];exact ⟨h9, h8⟩
      exact h7
   apply lt_abs.mpr;left;exact h6

lemma nonneg₁ [Setting E₁ E₂ F admm admm_kkt]: min τ (1 + τ - τ ^ 2) > 0 := by
   rcases admm.htau with ⟨h1, _⟩
   have h2 : 1 + τ - τ ^ 2 > 0 := nonneg_prime
   apply lt_min h1 h2

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
   apply lt_min one_pos h2

lemma Φ₁_nonneg [Setting E₁ E₂ F admm admm_kkt]:
∀ n : ℕ+ , 0 ≤ (min τ (1 + τ - τ ^ 2) ) * ρ * ‖A₂ (x₂ n - x₂ (n + 1))‖ ^ 2 := by
   intro n
   have ha: 0 < (min τ (1 + τ - τ ^ 2) ) * ρ := by
      apply mul_pos nonneg₁ ADMM.hrho
   have ha': 0 ≤ (min τ (1 + τ - τ ^ 2) ) * ρ := by apply le_of_lt ha
   have hb: 0 ≤ ‖A₂ (x₂ n - x₂ (n + 1))‖ ^ 2 := by apply sq_nonneg
   apply mul_nonneg ha' hb

lemma Φ₂_nonneg [Setting E₁ E₂ F admm admm_kkt]:
∀ n : ℕ+ ,  0 ≤ (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (n + 1)) + A₂ (e₂ (n + 1))‖ ^ 2 := by
   intro n
   have ha: 0 < (min 1 (1 + 1 / τ - τ )) * ρ := by
      apply mul_pos nonneg₂ ADMM.hrho
   have ha': 0 ≤ (min 1 (1 + 1 / τ - τ )) * ρ := by apply le_of_lt ha
   have hb: 0 ≤ ‖A₁ (e₁ (n + 1)) + A₂ (e₂ (n + 1))‖ ^ 2 := by apply sq_nonneg
   apply mul_nonneg ha' hb

lemma big_is_ge_zero [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+,
(min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ n - x₂ (n + 1))‖ ^ 2
+ (min 1 (1 + 1 / τ - τ)) * ρ * ‖A₁ (e₁ (n + 1)) + A₂ (e₂ (n + 1))‖ ^ 2
≥ 0 := by
   intro n
   have h1 :=Φ₁_nonneg n
   have h2 :=Φ₂_nonneg n
   apply add_nonneg h1 h2

lemma Φ_is_monotone [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+, Φ n ≥ Φ (n+1) := by
   intro n
   let c := (min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ n - x₂ (n + 1))‖ ^ 2
          + (min 1 (1 + 1 / τ - τ)) * ρ * ‖A₁ (e₁ (n + 1)) + A₂ (e₂ (n + 1))‖ ^ 2
   have h : c ≥ 0 := by apply big_is_ge_zero
   have h' : (Φ n) - (Φ (n + 1)) ≥ 0 := by
      calc
         _ ≥ c := by apply Φ_isdescending
         _ ≥ 0 := by apply h
   linarith [h']

lemma nonneg₃ [Setting E₁ E₂ F admm admm_kkt]: max (1 - τ) (1 - 1 / τ) ≥ 0 := by
   rcases τ_segment with h|h
   case inl
   => have ha : 1 - τ ≥ 1 - 1/τ := by
         apply sub_le_sub_left; rw [le_div_iff₀ (by linarith), ← sq]
         apply pow_le_one₀; repeat linarith
      rw [max_eq_left ha];linarith
   case inr
   => have hb : 1 - 1/τ ≥ 1 - τ := by
         have : 1 / τ ≤ 1 := by
            rw [one_div]
            apply inv_le_one_of_one_le₀; linarith
         linarith
      rw [max_eq_right hb];apply sub_nonneg_of_le
      rw [one_div];apply inv_le_one_of_one_le₀; linarith

lemma Φ_is_nonneg [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ , Φ n ≥ 0 := by
   intro n
   rcases admm.htau with ⟨h1, _⟩
   simp [Φ]
   have h2 : Ψ n ≥ 0 := by
      simp [Ψ];apply add_nonneg;repeat apply mul_nonneg
      apply inv_nonneg_of_nonneg; apply le_of_lt admm.hrho
      apply inv_nonneg_of_nonneg; apply le_of_lt h1
      apply pow_two_nonneg;apply mul_nonneg; apply le_of_lt admm.hrho; apply pow_two_nonneg
   have h3 : ((max (1 - τ) (1 - 1/τ)) * ρ) * ‖A₁ ((e₁) n) + A₂ ((e₂) n)‖ ^2 ≥ 0 := by
      repeat apply mul_nonneg
      apply nonneg₃
      apply le_of_lt admm.hrho
      apply pow_two_nonneg
   rw [← one_div];apply add_nonneg h2 h3

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
      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

lemma Φ_isBounded' [Setting E₁ E₂ F admm admm_kkt] : ∃ (r : ℝ), (range Φ) ⊆ ball 0 r := by
   rcases Φ_bd_above with ⟨C,bd⟩
   use C; intro x hx; simp; rw [range] at hx; simp at hx
   rcases hx with ⟨n,eq⟩; rw [← eq, abs_eq_self.2]; exact bd n
   apply Φ_is_nonneg

lemma Φ_isBounded [Setting E₁ E₂ F admm admm_kkt]: IsBounded (range Φ) := (isBounded_iff_subset_ball 0).2  Φ_isBounded'

lemma ey_isBounded' [Setting E₁ E₂ F admm admm_kkt]: ∃ (r : ℝ), (range ey) ⊆ ball 0 r := by
   rcases Φ_bd_above with ⟨r, Φ_isBounded⟩;
   use √(τ * ρ * r); intro x hx; simp; rw [range] at hx; simp at hx
   rcases hx with ⟨n, eq⟩; rw [← eq]
   have hτ : τ > 0 := by rcases admm.htau with ⟨h₁, _⟩; exact h₁
   have hρ : ρ > 0 := by exact admm.hrho
   have τ_mul_ρ' : τ * ρ > 0 := by apply mul_pos hτ hρ
   have τ_mul_ρ : τ * ρ ≥ 0 := by apply le_of_lt (mul_pos hτ hρ)
   have open_Φ (n : ℕ) : τ * ρ * Φ n = ‖ey n‖^2 + τ * ρ * ρ * ‖A₂ (e₂ n)‖ ^ 2 + τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^2 := by
      simp [Φ, Ψ]; ring_nf; rw [mul_assoc, mul_assoc, mul_assoc]; nth_rw 2 [← mul_assoc] ; rw [mul_inv_cancel₀, one_mul]
      rw [← mul_assoc, mul_inv_cancel₀, one_mul]; ring; apply ne_of_gt hτ; apply ne_of_gt hρ
   have open_Φ' (n : ℕ) :  ‖ey n‖^2 + τ * ρ * ρ * ‖A₂ (e₂ n)‖ ^ 2 + τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^2
      = ‖ey n‖^2 + (τ * ρ * ρ * ‖A₂ (e₂ n)‖ ^ 2 + τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^2) := by ring_nf
   have nonneg1 (n : ℕ): τ * ρ * ρ * ‖A₂ (e₂ n)‖ ^ 2 ≥ 0 := by
      have : τ * ρ * ρ > 0 := by apply mul_pos τ_mul_ρ' hρ
      apply mul_nonneg (le_of_lt this)
      apply pow_two_nonneg
   have nonneg2 (n : ℕ): τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^2 ≥ 0 := by
      have h2 : ((max (1 - τ) (1 - 1 / τ)) * ρ ) ≥ 0 := by
         apply (mul_nonneg_iff_left_nonneg_of_pos hρ).2
         apply nonneg₃
      have h3 : τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) ≥ 0 := by apply mul_nonneg τ_mul_ρ h2
      apply mul_nonneg h3
      apply pow_two_nonneg
   have nonneg3 (n : ℕ): τ * ρ * ρ * ‖A₂ (e₂ n)‖ ^ 2 + τ * ρ * ((max (1 - τ) (1 - 1 / τ)) * ρ ) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^2 ≥ 0 := by
      apply add_nonneg (nonneg1 n) (nonneg2 n)
   have ey_norm (n : ℕ): ‖ey n‖ ^ 2 ≤ τ * ρ * Φ n := by
      rw [open_Φ, open_Φ']; linarith [nonneg3 n]
   have ey_norm_pow (n : ℕ) : ‖ey n‖ ^ 2 < τ * ρ * r := by
      have Φ_lt_r :  τ * ρ * Φ n < τ * ρ * r := by apply mul_lt_mul_of_pos_left (Φ_isBounded n) τ_mul_ρ'
      apply lt_of_le_of_lt (ey_norm n) Φ_lt_r
   have ey_norm_above (n : ℕ) : ‖ey n‖ < √(τ * ρ * r) := by
      have h_ey: √(‖ey n‖^2) = ‖ey n‖ := by rw [pow_two]; apply Real.sqrt_mul_self; apply norm_nonneg
      rw [← h_ey]
      have : ‖ey n‖^2 ≥ 0 := by apply pow_two_nonneg
      apply (Real.sqrt_lt_sqrt_iff this).mpr
      exact ey_norm_pow n
   exact ey_norm_above n


lemma ey_isBounded [Setting E₁ E₂ F admm admm_kkt]: IsBounded (range ey ) := (isBounded_iff_subset_ball 0).2  ey_isBounded'

lemma unfold_Φ [Setting E₁ E₂ F admm admm_kkt]: ∀ n, ‖Φ n‖ = ‖1 / (τ * ρ) * ‖ey n‖ ^ 2
+ ρ * ‖A₂ (e₂ n)‖ ^ 2
+ max (1 - τ) (1 - 1 / τ) * ρ * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2‖ := by
   unfold Φ Ψ
   simp

lemma tau_pos : 0 < τ := by apply ADMM.htau.1

lemma rho_pos : 0 < ρ := by exact ADMM.hrho

lemma zero_le_tau_mul_rho : 0 ≤ τ * ρ := by
   have h : 0 < τ * ρ := by exact mul_pos tau_pos rho_pos
   apply le_of_lt h

lemma max_tau_nonneg [Setting E₁ E₂ F admm admm_kkt]: 0 ≤ max (1 - τ) (1 - 1 / τ) := by
   apply nonneg₃

lemma max_tau_mul_nonneg [Setting E₁ E₂ F admm admm_kkt]:∀ n, 0 ≤ max (1 - τ) (1 - 1 / τ) * ρ * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 :=by
   intro n
   apply mul_nonneg
   · apply mul_nonneg
      max_tau_nonneg; apply le_of_lt rho_pos
   · apply pow_nonneg; simp
lemma ineq1 [Setting E₁ E₂ F admm admm_kkt]: ∀ n, ρ * ‖A₂ (e₂ n)‖ ^ 2 ≤ ‖Φ n‖ := by
   intro n
   let x1 := 1 / (τ*ρ) * ‖ey n‖ ^ 2
   have hx1: 0 ≤ x1 := by
      apply mul_nonneg
      · apply div_nonneg
         zero_le_one; exact zero_le_tau_mul_rho
      · apply pow_nonneg; simp
   let x2 := ρ * ‖A₂ (e₂ n)‖ ^ 2
   have hx2: 0 ≤ x2 := by
      apply mul_nonneg
      · apply le_of_lt rho_pos
      · apply pow_nonneg; simp
   let x3 := max (1 - τ) (1 - 1 / τ) * ρ * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2
   have hx3: 0 ≤ x3 := by apply max_tau_mul_nonneg

   have h: ρ * ‖A₂ (e₂ n)‖ ^ 2 ≤ ‖Φ n‖ ↔ x2 ≤ ‖x1 + x2 + x3‖ := by rw[unfold_Φ]
   have h_norm_pos : 0 ≤ ‖x1 + x2 + x3‖ := by exact norm_nonneg (x1 + x2 + x3)
   have h_norm_eq : ‖x1 + x2 + x3‖ = x1 + x2 + x3 := by rw [Real.norm_of_nonneg];linarith [hx1, hx2, hx3]

   have htrans: x2 ≤ ‖x1 + x2 + x3‖ := by linarith [hx2, h_norm_pos]
   exact (h.mpr htrans)

lemma Φn_isBounded [Setting E₁ E₂ F admm admm_kkt]: ∃ r_Φ , ∀ n, ‖Φ n‖ < r_Φ := by
   have hΦ : ∃ r_Φ, range Φ ⊆ Metric.ball 0 r_Φ := by apply Φ_isBounded'
   rcases hΦ with ⟨r_Φ, hΦ⟩
   use r_Φ
   intro n
   have h0 : Φ n ∈ range Φ := by use n
   have h_in_ball : Φ n ∈ Metric.ball 0 r_Φ := by
      apply hΦ h0
   rw [Metric.mem_ball, dist_zero_right] at h_in_ball
   exact h_in_ball

lemma A₂e₂_isBounded' [Setting E₁ E₂ F admm admm_kkt]: ∃ (r : ℝ), (range (A₂ ∘ e₂) ) ⊆ ball 0 r := by

   rcases Φn_isBounded with ⟨r_Φ, h1⟩

   let r := √ (r_Φ / ρ)
   have hr : r = √ (r_Φ / ρ) := by rfl
   use r
   intros x hx
   rcases hx with ⟨n, rfl⟩

   have h2 : ρ * ‖A₂ (e₂ n)‖ ^ 2 ≤ ‖Φ n‖ := by apply ineq1

   have h3 : ρ * ‖A₂ (e₂ n)‖ ^ 2 < r_Φ := by
      calc
      ρ * ‖A₂ (e₂ n)‖ ^ 2 ≤ ‖Φ n‖ := h2
      _ < r_Φ := h1 n

   have h4 : 0 ≤ ‖A₂ (e₂ n)‖ := by
      apply norm_nonneg

   have h5: ‖A₂ (e₂ n)‖ < √ (r_Φ / ρ) := by
      calc ‖A₂ (e₂ n)‖
         = √ ((‖A₂ (e₂ n)‖) ^ 2) := by conv in ‖A₂ (e₂ n)‖ => rw [← Real.sqrt_sq h4];rfl
         _ < √ (r_Φ / ρ) := by
            rw [← lt_div_iff₀' ADMM.hrho] at h3
            apply Real.sqrt_lt_sqrt at h3
            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

   rw [← hr] at h6
   rw [← Metric.mem_ball] at h6
   apply h6

lemma A₂e₂_isBounded [Setting E₁ E₂ F admm admm_kkt]: IsBounded (range (A₂ ∘ e₂) ) :=
   (isBounded_iff_subset_ball 0).2 A₂e₂_isBounded'

lemma Φ_sub_nonneg [Setting E₁ E₂ F admm admm_kkt]: ∀ n : ℕ+ , 0 ≤ (Φ n) - (Φ (n + 1)) := by
   intro n
   have h := big_is_ge_zero n
   apply le_trans
   · apply h
   · apply Φ_isdescending

lemma ineq2 [Setting E₁ E₂ F admm admm_kkt]: 0 < min 1 (1 + 1 / τ - τ ) * ρ := by apply mul_pos nonneg₂ ADMM.hrho

lemma A₁e₁_A₂e₂_isBounded'[Setting E₁ E₂ F admm admm_kkt] : ∃ (r : ℝ), (range (A₁ ∘ e₁ + A₂ ∘ e₂) ) ⊆ ball 0 r := by
   -- obtain r_Φ
   have hΦ : ∃ r_Φ, range Φ ⊆ Metric.ball 0 r_Φ := by apply Φ_isBounded'
   rcases hΦ with ⟨r_Φ, hΦ⟩

   -- h1 ~ h5 : n ≥ 1 (n : ℕ +)
   have h1 (k : ℕ+): (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2 ≤
   (min τ (1 + τ - τ ^ 2) )* ρ * ‖A₂ (x₂ k - x₂ (k + 1))‖ ^ 2 +
   (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2 := by
      have h1' : 0 ≤ (min τ (1 + τ - τ ^ 2) ) * ρ * ‖A₂ (x₂ k - x₂ (k + 1))‖ ^ 2 := by
         have ha: 0 < (min τ (1 + τ - τ ^ 2) ) * ρ := by
            apply mul_pos nonneg₁ ADMM.hrho
         have ha': 0 ≤ (min τ (1 + τ - τ ^ 2) ) * ρ := by apply le_of_lt ha
         have hb: 0 ≤ ‖A₂ (x₂ k - x₂ (k + 1))‖ ^ 2 := by apply sq_nonneg
         apply mul_nonneg ha' hb
      linarith

   have h2 (k : ℕ+): (min τ (1 + τ - τ ^ 2) ) * ρ * ‖A₂ (x₂ k - x₂ (k + 1))‖ ^ 2 + (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2 ≤ (Φ k) - (Φ (k + 1)) := by
      apply Φ_isdescending

   have h3 (k : ℕ+): (Φ k) - (Φ (k + 1)) < 2 * r_Φ := by
      have h3a: ‖Φ k‖ < r_Φ := by
         have h3a': Φ k ∈ range Φ := by use k
         have h_in_ball : Φ k ∈ Metric.ball 0 r_Φ := by apply hΦ h3a'
         rw [Metric.mem_ball, dist_zero_right] at h_in_ball
         exact h_in_ball
      have h3b: ‖Φ (k+1)‖ < r_Φ := by
         have h3b': Φ (k+1) ∈ range Φ := by use (k+1)
         have h_in_ball : Φ (k+1) ∈ Metric.ball 0 r_Φ := by apply hΦ h3b'
         rw [Metric.mem_ball, dist_zero_right] at h_in_ball
         exact h_in_ball
      have h3': ‖Φ k‖ + ‖Φ (k+1)‖ < r_Φ + r_Φ := by apply add_lt_add h3a h3b
      have h3'': ‖Φ k‖ + ‖Φ (k+1)‖ < 2 * r_Φ := by linarith [h3']
      have h3aa: ‖(Φ k) - (Φ (k + 1))‖ ≤ ‖Φ k‖ + ‖Φ (k+1)‖ := by apply norm_sub_le
      have h3bb: (Φ k) - (Φ (k + 1)) = ‖(Φ k) - (Φ (k + 1))‖ := by
         refine Eq.symm (Real.norm_of_nonneg ?hr); exact Φ_sub_nonneg k
      rw [h3bb]
      exact lt_of_le_of_lt h3aa h3''

   have h4 (k : ℕ+): ((min 1 (1 + 1 / τ - τ )) * ρ) * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2 < 2 * r_Φ := by
      calc (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2
         _ ≤ (min τ (1 + τ - τ ^ 2) )* ρ * ‖A₂ (x₂ k - x₂ (k + 1))‖ ^ 2 + (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ ^ 2 := h1 k
         _ ≤ (Φ k) - (Φ (k + 1)) := h2 k
         _ < 2 * r_Φ := h3 k

   have h5 (k : ℕ+): ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ < √ (2 * r_Φ / ((min 1 (1 + 1 / τ - τ )) * ρ)) := by
      have h4_ins := h4 k
      have h5a: 0 ≤ ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ := by apply norm_nonneg
      calc ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖
         _ = √ ((‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖) ^ 2) := by conv in ‖A₁ (e₁ (k + 1)) + A₂ (e₂ (k + 1))‖ => rw [← Real.sqrt_sq h5a];rfl
         _ < √ (2 * r_Φ / ((min 1 (1 + 1 / τ - τ )) * ρ)) := by
            rw [← lt_div_iff₀' ineq2] at h4_ins
            apply Real.sqrt_lt_sqrt at h4_ins
            exact h4_ins; simp

   have h5' (n : ℕ) (hn : 1 < n): ‖A₁ (e₁ n) + A₂ (e₂ n)‖ < √ (2 * r_Φ / ((min 1 (1 + 1 / τ - τ )) * ρ)) := by
      have h_pos : 0 < n - 1 := by exact Nat.zero_lt_sub_of_lt hn
      let k : ℕ+ := (n-1).toPNat h_pos
      have h_k := h5 k
      have k_to_n : k = n - 1 := by rfl
      rw [k_to_n] at h_k
      rw [Nat.sub_add_cancel] at h_k
      exact h_k
      apply le_of_lt hn

   have h_n0 : ‖A₁ (e₁ 0) + A₂ (e₂ 0)‖ < ‖A₁ (e₁ 0) + A₂ (e₂ 0)‖ + 1 := by linarith

   have h_n1 : ‖A₁ (e₁ 1) + A₂ (e₂ 1)‖ < ‖A₁ (e₁ 1) + A₂ (e₂ 1)‖ + 1 := by linarith

   let r := (max (max (√ (2 * r_Φ / ((min 1 (1 + 1 / τ - τ )) * ρ))) (‖A₁ (e₁ 0) + A₂ (e₂ 0)‖ + 1 )) (‖A₁ (e₁ 1) + A₂ (e₂ 1)‖ + 1 ))
   have hr' : r = (max (max (√ (2 * r_Φ / ((min 1 (1 + 1 / τ - τ )) * ρ))) (‖A₁ (e₁ 0) + A₂ (e₂ 0)‖ + 1 )) (‖A₁ (e₁ 1) + A₂ (e₂ 1)‖ + 1 )) := by rfl
   use r

   intros x hx
   rcases hx with ⟨n, rfl⟩

   -- combine h5' h_n0 h_n1 together
   have h_n (n : ℕ): ‖A₁ (e₁ n) + A₂ (e₂ n)‖ < r := by

      by_cases hn0 : n = 0
      rw [hn0]
      apply lt_of_lt_of_le h_n0
      rw [hr', max_assoc, max_left_comm]
      apply le_max_left

      by_cases hn1 : n = 1
      rw [hn1]
      apply lt_of_lt_of_le h_n1
      rw [hr']; apply le_max_right
      have hn : 1 < n := by
         exact Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
      apply lt_of_lt_of_le (h5' n hn)
      rw [hr']
      rw [max_assoc]; apply le_max_left

   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'

   rw [← Metric.mem_ball] at h6; simp; simp at h6
   exact h6

lemma A₁e₁_A₂e₂_isBounded [Setting E₁ E₂ F admm admm_kkt]: IsBounded (range (A₁ ∘ e₁ + A₂ ∘ e₂) ) :=
   (isBounded_iff_subset_ball 0).2 A₁e₁_A₂e₂_isBounded'

lemma A₁e₁_isBounded' [Setting E₁ E₂ F admm admm_kkt]: ∃ (r : ℝ), range (A₁ ∘ e₁) ⊆ ball 0 r := by

   have h_A₂e₂ : ∃ r1, range (A₂ ∘ e₂) ⊆ ball 0 r1 := by apply A₂e₂_isBounded'
   rcases h_A₂e₂ with ⟨r1, h_A₂e₂⟩

   have h_A₁e₁_A₂e₂ : ∃ r2, range (A₁ ∘ e₁ + A₂ ∘ e₂) ⊆ ball 0 r2 := by apply A₁e₁_A₂e₂_isBounded'
   rcases h_A₁e₁_A₂e₂ with ⟨r2, h_A₁e₁_A₂e₂⟩

   let r := r1 + r2
   have hr : r = r1 + r2 := by rfl
   use r

   intros x hx
   rcases hx with ⟨n, rfl⟩

   have h : ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖ < r1 + r2 := by
      have ha : ‖A₂ (e₂ n)‖ < r1 := by
         have haa : A₂ (e₂ n) ∈ range (A₂ ∘ e₂) := by use n; simp
         have ha_in_ball : A₂ (e₂ n) ∈ Metric.ball 0 r1 := by apply h_A₂e₂ haa
         rw [Metric.mem_ball, dist_zero_right] at ha_in_ball
         exact ha_in_ball
      have hb : ‖A₁ (e₁ n) + A₂ (e₂ n)‖ < r2 := by
         have hbb : A₁ (e₁ n) + A₂ (e₂ n) ∈ range (A₁ ∘ e₁ + A₂ ∘ e₂) := by use n; simp
         have hb_in_ball : A₁ (e₁ n) + A₂ (e₂ n) ∈ Metric.ball 0 r2 := by apply h_A₁e₁_A₂e₂ hbb
         rw [Metric.mem_ball, dist_zero_right] at hb_in_ball
         exact hb_in_ball
      linarith

   have h_ineq : ‖A₁ (e₁ n)‖ ≤ ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖ := by apply norm_le_add_norm_add

   have h_norm : ‖A₁ (e₁ n)‖ < r := by
      calc ‖A₁ (e₁ n)‖
         _ ≤ ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖ := h_ineq
         _ < r1 + r2 := h
         _ = 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

   rw [← Metric.mem_ball] at h_dist
   apply h_dist

lemma A₁e₁_isBounded [Setting E₁ E₂ F admm admm_kkt]: IsBounded (range (A₁ ∘ e₁) ) :=
   (isBounded_iff_subset_ball 0).2 A₁e₁_isBounded'

lemma open_mapping_e₁ [Setting E₁ E₂ F admm admm_kkt] (fullrank₁: Function.Injective admm.A₁):
      ∃ C > 0, ∀ n : ℕ, ‖e₁ n‖ ≤ C * ‖A₁ (e₁ n)‖ := by
   rcases inv_bounded₂ A₁ fullrank₁ with ⟨C, ⟨C_pos,hh⟩⟩
   use C; constructor
   ·  exact C_pos
   ·  intro n; exact hh (e₁ n)

lemma open_mapping_e₂ [Setting E₁ E₂ F admm admm_kkt] (fullrank₂: Function.Injective admm.A₂):
      ∃ C > 0, ∀ n : ℕ, ‖e₂ n‖ ≤ C * ‖A₂ (e₂ n)‖ := by
   rcases inv_bounded₂ A₂ fullrank₂ with ⟨C, ⟨C_pos,hh⟩⟩
   use C; constructor
   ·  exact C_pos
   ·  intro n; exact hh (e₂ n)

lemma x₁_isBounded' [Setting E₁ E₂ F admm admm_kkt](fullrank₁: Function.Injective admm.A₁): ∃ (r : ℝ), (range x₁) ⊆ ball 0 r := by
   rcases A₁e₁_isBounded' with ⟨M, h₁⟩
   rcases open_mapping_e₁ fullrank₁ with ⟨C, ⟨C_pos, h₂⟩⟩
   rw [range] at h₁
   use C * M + ‖x₁'‖; intro x hx; rw [range] at hx; simp at hx
   rcases hx with ⟨n,eq⟩
   have A₁e₁_bd : ‖A₁ (e₁ n)‖ < M := by
      have : A₁ (e₁ n) ∈ {x | ∃ n, A₁ (e₁ n) = x} := by simp
      have : A₁ (e₁ n) ∈ ball 0 M := by tauto
      simp at this; exact this
   rw [← eq]; simp
   calc
      _ = ‖(x₁ n - x₁') + x₁'‖ := by rw [add_comm, add_sub, add_comm, add_sub_assoc, sub_self, add_zero]
      _ ≤ ‖x₁ n - x₁'‖ + ‖x₁'‖ := by apply norm_add_le
      _ = ‖e₁ n‖ + ‖x₁'‖ := by rw [e₁]
      _ ≤ C * ‖A₁ (e₁ n)‖ + ‖x₁'‖ := by linarith [h₂ n]
      _ < C * M + ‖x₁'‖ := by linarith [mul_lt_mul_of_pos_left A₁e₁_bd C_pos]

lemma x₁_isBounded [Setting E₁ E₂ F admm admm_kkt](fullrank₁: Function.Injective admm.A₁):
      IsBounded (range x₁) :=
   (isBounded_iff_subset_ball 0).2 (x₁_isBounded' fullrank₁)

lemma x₂_isBounded' [Setting E₁ E₂ F admm admm_kkt] (fullrank₂: Function.Injective admm.A₂):
      ∃ (r : ℝ), (range x₂ ) ⊆ ball 0 r := by
   rcases A₂e₂_isBounded' with ⟨M, h₁⟩
   rcases open_mapping_e₂ fullrank₂ with ⟨C, ⟨C_pos, h₂⟩⟩
   rw [range] at h₁
   use C * M + ‖x₂'‖; intro x hx; rw [range] at hx; simp at hx
   rcases hx with ⟨n,eq⟩
   have A₂e₂_bd : ‖A₂ (e₂ n)‖ < M := by
      have : A₂ (e₂ n) ∈ {x | ∃ n, A₂ (e₂ n) = x} := by simp
      have : A₂ (e₂ n) ∈ ball 0 M := by tauto
      simp at this; exact this
   rw [← eq]; simp
   calc
      _ = ‖(x₂ n - x₂') + x₂'‖ := by rw [add_comm, add_sub, add_comm, add_sub_assoc, sub_self, add_zero]
      _ ≤ ‖x₂ n - x₂'‖ + ‖x₂'‖ := by apply norm_add_le
      _ = ‖e₂ n‖ + ‖x₂'‖ := by rw [e₂]
      _ ≤ C * ‖A₂ (e₂ n)‖ + ‖x₂'‖ := by linarith [h₂ n]
      _ < C * M + ‖x₂'‖ := by linarith [mul_lt_mul_of_pos_left A₂e₂_bd C_pos]

lemma x₂_isBounded [Setting E₁ E₂ F admm admm_kkt] (fullrank₂: Function.Injective admm.A₂):
      IsBounded (range x₂) :=
   (isBounded_iff_subset_ball 0).2 (x₂_isBounded' fullrank₂)

lemma y_isBounded' [Setting E₁ E₂ F admm admm_kkt] :
      ∃ (r : ℝ), (range y) ⊆ ball 0 r := by
   rcases ey_isBounded' with ⟨M, h⟩
   use M + ‖y'‖; intro x hx; rw [range] at hx h; simp at hx; simp
   rcases hx with ⟨n,eq⟩; rw [← eq]
   have ey_bd : ‖ey n‖ < M := by
      have : ey n ∈ {x | ∃ n, ey n = x} := by simp
      have : ey n ∈ ball 0 M := by tauto
      simp at this; exact this
   calc
      _ = ‖(y n) - y' + y'‖ := by rw [add_comm, add_sub, add_comm, add_sub_assoc, sub_self, add_zero]
      _ ≤ ‖y n - y'‖ + ‖y'‖ := by apply norm_add_le
      _ = ‖ey n‖ + ‖y'‖ := by rw [ey]
      _ < M + ‖y'‖ := by linarith

lemma y_isBounded  [Setting E₁ E₂ F admm admm_kkt]:  IsBounded (range y) :=
   (isBounded_iff_subset_ball 0).2  y_isBounded'


lemma times_eq : (range (fun n => (x₁ n,  x₂ n, y n ) ))
⊆  (range x₁) ×ˢ  (range x₂) ×ˢ (range y) := by
   simp [range]
   intro x hx
   dsimp at hx
   simp only [mem_prod, mem_setOf_eq]
   rcases hx with ⟨n , hn⟩
   have h1 : x₁ n = x.1 := hn.symm ▸ rfl
   have h2 : x₂ n = x.2.1 := hn.symm ▸ rfl
   have h3 : y  n = x.2.2 := hn.symm ▸ rfl
   exact ⟨ ⟨ n , h1 ⟩, ⟨ n , h2 ⟩, ⟨ n , h3 ⟩⟩


lemma xy_isBounded [Setting E₁ E₂ F admm admm_kkt]
      (fullrank₁: Function.Injective admm.A₁) (fullrank₂: Function.Injective admm.A₂):
      IsBounded (range (fun n => (x₁ n,  x₂ n, y n ) )) := by
   apply IsBounded.subset
   apply IsBounded.prod (x₁_isBounded fullrank₁)
   apply IsBounded.prod (x₂_isBounded fullrank₂) y_isBounded
   apply times_eq

structure Converge_Subseq [Setting E₁ E₂ F admm admm_kkt] where
   x₁'' : E₁
   x₂'' : E₂
   y''  : F
   φ    : ℕ → ℕ
   hphi:StrictMono φ
   hconverge:Tendsto (fun n => (x₁ (φ n),  x₂ (φ n), y (φ n))) atTop (𝓝 (x₁'' , x₂'' , y''))

def Subseq [Setting E₁ E₂ F admm admm_kkt]
      (fullrank₁: Function.Injective admm.A₁) (fullrank₂: Function.Injective admm.A₂): Converge_Subseq := by
   let x := tendsto_subseq_of_bounded (xy_isBounded fullrank₁ fullrank₂)
      (inSet (fun n => (x₁ n,  x₂ n, y n )) )
   choose x hx using x
   choose φ hphi1 using hx.2
   exact
      {
         x₁'' := x.1
         x₂'' := x.2.1
         y''  := x.2.2
         φ   := φ
         hphi:= hphi1.1
         hconverge:=hphi1.2
      }

variable (fullrank₁: Function.Injective admm.A₁) (fullrank₂: Function.Injective admm.A₂)
-- Subsequence mapping
local notation "φ" => Converge_Subseq.φ (Subseq fullrank₁ fullrank₂)

-- The limit of the subsequence
local notation "x₁''" => Converge_Subseq.x₁'' (Subseq fullrank₁ fullrank₂)
local notation "x₂''" => Converge_Subseq.x₂'' (Subseq fullrank₁ fullrank₂)
local notation "y''"  => Converge_Subseq.y'' (Subseq fullrank₁ fullrank₂)

-- The subsequence mapping is strictly increasing
lemma hphi_StrictMono [Setting E₁ E₂ F admm admm_kkt] : StrictMono φ := (Subseq fullrank₁ fullrank₂).hphi

--lim_{n → ∞} (uₙ ,vₙ ) = 0 -> lim_{n → ∞} uₙ  = 0
lemma admm_nhds_prod_eq [Setting E₁ E₂ F admm admm_kkt] : 𝓝 (x₁'' , x₂'' , y'') = 𝓝 x₁'' ×ˢ 𝓝 x₂'' ×ˢ 𝓝 y'' := by
   rw[nhds_prod_eq,nhds_prod_eq]

lemma hconverge [Setting E₁ E₂ F admm admm_kkt]  : Tendsto (fun n => (x₁ (φ n),  x₂ (φ n), y (φ n)))
atTop (𝓝 x₁'' ×ˢ 𝓝 x₂'' ×ˢ 𝓝 y''):=by
   have := (Subseq fullrank₁ fullrank₂).hconverge
   rw[admm_nhds_prod_eq] at this
   exact this

lemma x₁_subseq_converge [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (x₁ (φ n)))  atTop (𝓝 x₁'') :=
   (Filter.tendsto_prod_iff'.1 (hconverge fullrank₁ fullrank₂)).1

lemma x₂_subseq_converge [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (x₂ (φ n)))  atTop (𝓝 x₂'') :=
   (Filter.tendsto_prod_iff'.1 (Filter.tendsto_prod_iff'.1 (hconverge fullrank₁ fullrank₂)).2).1

lemma y_subseq_converge  [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (y (φ n)))  atTop (𝓝 y'') :=
   (Filter.tendsto_prod_iff'.1 (Filter.tendsto_prod_iff'.1 (hconverge fullrank₁ fullrank₂)).2).2

def φ₁' [Setting E₁ E₂ F admm admm_kkt] : ℕ → ℕ+ := by
   intro n
   exact (φ (n + 1)).toPNat'

local notation "φ₁" => φ₁' fullrank₁ fullrank₂

lemma φ₁_equ [Setting E₁ E₂ F admm admm_kkt] [Setting E₁ E₂ F admm admm_kkt] : ∀ n : ℕ , φ₁ n = φ (n + 1) := by
   intro n
   have : φ (n + 1) > 0 := by
      calc φ (n + 1)
         _ ≥ n + 1  := StrictMono.id_le (hphi_StrictMono fullrank₁ fullrank₂) (n + 1)
         _ > 0      :=by linarith
   exact Nat.sub_one_add_one_eq_of_pos this

-- lim_{ n → ∞} x_n  = x =>  lim_{ n → ∞} x_{n+1}  = x
lemma x₁_subseq_converge' [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (x₁ (φ₁ n)))  atTop (𝓝 x₁'') :=by
   have : (fun n => x₁ (φ₁ n)) = (fun n => (x₁ (φ (n+1)))) :=by
      ext n;rw[φ₁_equ fullrank₁ fullrank₂ n]
   rw[this , Filter.tendsto_add_atTop_iff_nat (f := (fun n ↦ x₁ (φ n)) ) 1]
   apply x₁_subseq_converge

lemma x₂_subseq_converge' [Setting E₁ E₂ F admm admm_kkt]  : Tendsto (fun n => (x₂ (φ₁ n)))  atTop (𝓝 x₂'') :=by
   have : (fun n => x₂ (φ₁ n)) = (fun n => (x₂ (φ (n+1)))) :=by
      ext n;rw[φ₁_equ fullrank₁ fullrank₂ n]
   rw[this , Filter.tendsto_add_atTop_iff_nat (f := (fun n ↦ x₂ (φ n)) ) 1]
   apply x₂_subseq_converge

lemma Φ_Summable₁' [Setting E₁ E₂ F admm admm_kkt] :
      ∃ (c : ℝ) , ∀ (n : ℕ), ∑ i ∈ Finset.range n, ((Φ i.succ ) - (Φ (i.succ + 1))) ≤ c := by
   rcases Φn_isBounded with ⟨r , hr⟩
   use r + r
   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]
   have h : Finset.range n =Finset.range n := rfl
   rw[← Finset.sum_congr h this , Finset.sum_range_sub']
   simp only [φ₀]
   calc Φ (Nat.succ 0) - Φ n.succ
      _ ≤ |Φ (Nat.succ 0) - Φ n.succ|:=by apply le_abs_self
      _ ≤ |Φ (Nat.succ 0)| + |Φ n.succ|:= by apply abs_sub
      _ ≤ r + r := by
         apply le_of_lt
         apply add_lt_add (hr (Nat.succ 0)) (hr (Nat.succ n))

lemma Φ_isSummable [Setting E₁ E₂ F admm admm_kkt] : Summable (fun n : ℕ => (Φ (n+1) ) - (Φ (n+1 + 1))) := by
   rcases Φ_Summable₁'  with ⟨c , hn⟩
   apply summable_of_sum_range_le (c:=c)
   intro n
   have :n + 1 > 0 := by linarith
   apply Φ_sub_nonneg (n + 1).toPNat'
   exact hn

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

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
   calc (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (m+1)) + A₂ (e₂ (m+1))‖ ^ 2
      _≤ (min τ (1 + τ - τ ^ 2) )* ρ * ‖A₂ ((x₂ m )- x₂ (m + 1))‖ ^ 2
       + (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (m + 1)) + A₂ (e₂ (m + 1))‖ ^ 2:=by
         simp only [one_div, le_add_iff_nonneg_left]
         exact Φ₁_nonneg m
      _≤ Φ m - Φ (m + 1) := by apply Φ_isdescending

lemma Summable₁' [Setting E₁ E₂ F admm admm_kkt] :
      ∀ (n : ℕ), (fun n => (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (n+2)) + A₂ (e₂ (n+2))‖^2)  n
      ≤ (fun n : ℕ => (Φ (n+1) ) - (Φ (n+1 + 1))) n :=by
   intro n
   simp only
   let m := (n+1).toPNat'
   show (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (m+1)) + A₂ (e₂ (m+1))‖ ^ 2 ≤ Φ m - Φ (m + 1)
   apply Φ_inequ₁

lemma Summable₁ [Setting E₁ E₂ F admm admm_kkt] : Summable (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖^2) :=by
   let φn := fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2
   let φnsucc := fun n => (φn (n+2))
   show Summable φn
   rw[← summable_nat_add_iff 2]
   show Summable (fun n => φnsucc n)
   have φn_ge_zero': ∀ n , (min 1 (1 + 1 / τ - τ )) * ρ * φnsucc n ≥ 0 :=by
      intro n
      apply Φ₂_nonneg (n+1).toPNat'
   have h : (min 1 (1 + 1 / τ - τ )) * ρ ≠ 0 := by
      linarith [mul_pos nonneg₂ admm.hrho]
   rw[← summable_mul_left_iff h]
   apply summable_of_nonneg_of_le φn_ge_zero' Summable₁'
   apply Φ_isSummable

lemma  Φ_inequ₂ [Setting E₁ E₂ F admm admm_kkt] (m : ℕ+) :
      (min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ (m + 1) - x₂ m)‖^2 ≤ Φ m - Φ (m + 1) := by
   calc (min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ (m + 1) - x₂ m)‖^2
      _≤ (min τ (1 + τ - τ ^ 2) )* ρ * ‖A₂ ((x₂ m )- x₂ (m + 1))‖ ^ 2
       + (min 1 (1 + 1 / τ - τ )) * ρ * ‖A₁ (e₁ (m + 1)) + A₂ (e₂ (m + 1))‖ ^ 2:=by
         rw[norm_comm A₂ (x₂ (m + 1)) (x₂ m)]
         simp only [map_sub, le_add_iff_nonneg_right]
         exact Φ₂_nonneg m
      _≤ Φ m - Φ (m + 1) := by apply Φ_isdescending

lemma Summable₂' [Setting E₁ E₂ F admm admm_kkt] :
      ∀ (n : ℕ), (fun n =>(min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ (n + 1+ 1) - x₂ (n+1))‖^2) n
      ≤ (fun n : ℕ => (Φ (n+1) ) - (Φ (n+1 + 1))) n :=by
   intro n
   simp only
   let m := (n+1).toPNat'
   show (min τ (1 + τ - τ ^ 2)) * ρ * ‖A₂ (x₂ (m + 1) - x₂ m)‖^2 ≤ Φ m - Φ (m + 1)
   apply Φ_inequ₂

-- variable [Setting E₁ E₂ F admm admm_kkt]
lemma Summable₂ [Setting E₁ E₂ F admm admm_kkt]: Summable (fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖^2) :=by
   let φn := fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖^2
   let φnsucc := fun n => (φn (n+1))
   show Summable φn
   rw[← summable_nat_add_iff 1]
   show Summable (fun n => φnsucc n)
   have φn_ge_zero : ∀ n ,(min τ (1 + τ - τ ^ 2) )* ρ * φnsucc n ≥ 0 :=by
      intro n
      simp only [φnsucc , φn]
      rw[norm_comm A₂ (x₂ (n + 1 + 1)) (x₂ (n + 1))]
      apply Φ₁_nonneg (n+1).toPNat'
   have h : (min τ (1 + τ - τ ^ 2)) * ρ ≠ 0 := by
      linarith [mul_pos nonneg₁ admm.hrho]
   rw[← summable_mul_left_iff h]
   apply summable_of_nonneg_of_le φn_ge_zero Summable₂'
   apply Φ_isSummable

lemma y_subseq_converge' [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (y (φ₁ n))) atTop (𝓝 y'') := by
   have : (fun n => y (φ₁ n)) = (fun n => (y (φ (n+1)))) := by
      ext n; rw [φ₁_equ fullrank₁ fullrank₂ n]
   rw[this , Filter.tendsto_add_atTop_iff_nat (f := (fun n ↦ y (φ n)) ) 1]
   apply y_subseq_converge

lemma square_converge_zero₁ [Setting E₁ E₂ F admm admm_kkt]  (h : Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2)  atTop (𝓝 0)) :
   Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖)  atTop (𝓝 0) := by
   have : Tendsto (fun n => √((‖A₁ (e₁ n) + A₂ (e₂ n)‖)^2))  atTop (𝓝 √0) := by apply Filter.Tendsto.sqrt h
   rw [Real.sqrt_zero] at this; simp at this; exact this

-- ‖A₁ (e₁ n) + A₂ (e₂ n)‖ → 0
lemma converge_zero₁ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖)  atTop (𝓝 0) := by
   have : Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2)  atTop (𝓝 0) := by apply Summable.tendsto_atTop_zero Summable₁
   apply square_converge_zero₁ this

-- ‖A₁ (x₁ n) + A₂ (x₂ n) - b‖ → 0
lemma converge_zero₂ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => ‖A₁ (x₁ n) + A₂ (x₂ n) - b‖)  atTop (𝓝 0) := by
   have eq : (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖) = (fun n => ‖A₁ (x₁ n) + A₂ (x₂ n) - b‖) := by
      funext n
      have : A₁ (e₁ n) + A₂ (e₂ n) = A₁ (x₁ n) + A₂ (x₂ n) - b := by
         rw [e₁, e₂]; simp
         calc
            _ = A₁ (x₁ n) + A₂ (x₂ n) - ((A₁ x₁') + (A₂ x₂')) := by rw [sub_add_sub_comm]
            _ = A₁ (x₁ n) + A₂ (x₂ n) - b + b - ((A₁ x₁') + (A₂ x₂')) := by rw [sub_add_cancel]
            _ = A₁ (x₁ n) + A₂ (x₂ n) - b := by rw [Satisfaction_ofthekkt.eq]; simp
      rw [this]
   rw [← eq]
   exact converge_zero₁

-- with the square norm of A₂ (x₂ (n + 1) - x₂ n) → 0, we can infer that the norm of A₂ (x₂ (n + 1) - x₂ n) also → 0
lemma square_converge_zero₃ [Setting E₁ E₂ F admm admm_kkt] (h : Tendsto (fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖ ^ 2)  atTop (𝓝 0)) :
   Tendsto (fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖)  atTop (𝓝 0) := by
   have : Tendsto (fun n => √((‖A₂ (x₂ (n + 1) - x₂ n)‖)^2))  atTop (𝓝 √0) := by apply Filter.Tendsto.sqrt h
   rw [Real.sqrt_zero] at this; simp [Real.sqrt_sq] at this; simp; exact this

-- the norm of A₂ (x₂ (n + 1) - x₂ n) → 0
lemma converge_zero₃ [Setting E₁ E₂ F admm admm_kkt]  : Tendsto (fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖)  atTop (𝓝 0) := by
   have : Tendsto (fun n => ‖A₂ (x₂ (n + 1) - x₂ n)‖ ^ 2)  atTop (𝓝 0) := by
      apply Summable.tendsto_atTop_zero Summable₂
   apply square_converge_zero₃ this

-- A₁ (e₁ n) + A₂ (e₂ n) → 0 (Note that this lemma is without the norm)
lemma Seq_converge_zero₁ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₁ (e₁ n) + A₂ (e₂ n))  atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.2 converge_zero₁

-- A₁ (x₁ n) + A₂ (x₂ n) - b → 0
lemma Seq_converge_zero₂ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₁ (x₁ n) + A₂ (x₂ n) - b)  atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.2 converge_zero₂

-- A₂ (x₂ (n + 1) - x₂ n) → 0
lemma Seq_converge_zero₃ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₂ (x₂ (n + 1) - x₂ n))  atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.2 converge_zero₃

-- A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n)) → 0
lemma sub_Seq_converge_zero₁ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n)))
atTop (𝓝 0) := by
   apply Filter.tendsto_iff_seq_tendsto.1 Seq_converge_zero₁
   apply StrictMono.tendsto_atTop
   have : (fun n => (Int.toNat (φ₁ n))) = (fun n => (φ (n+1))) := by
      ext n; rw [φ₁_equ fullrank₁ fullrank₂ n]; simp
   simp at this; rw [this]
   apply StrictMono.comp
   · apply hphi_StrictMono
   · simp [StrictMono]

-- A₁ (x₁ (φ₁ n)) + A₂ (x₂ (φ₁ n)) - b → 0
lemma sub_Seq_converge_zero₂ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₁ (x₁ (φ₁ n)) + A₂ (x₂ (φ₁ n)) - b) atTop (𝓝 0) := by
   apply Filter.tendsto_iff_seq_tendsto.1 Seq_converge_zero₂
   apply StrictMono.tendsto_atTop
   have : (fun n => (Int.toNat (φ₁ n))) = (fun n => (φ (n+1))) := by
      ext n; rw [φ₁_equ fullrank₁ fullrank₂ n]; simp
   simp at this; rw [this]
   apply StrictMono.comp
   · apply hphi_StrictMono
   · simp [StrictMono]

-- A₂ (x₂ ((φ₁ n) + 1) - x₂ (φ₁ n)) → 0
lemma sub_Seq_converge_zero₃ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₂ (x₂ ((φ₁ n) + 1) - x₂ (φ₁ n))) atTop (𝓝 0) := by
   apply Filter.tendsto_iff_seq_tendsto.1 Seq_converge_zero₃
   apply StrictMono.tendsto_atTop
   have : (fun n => (Int.toNat (φ₁ n))) = (fun n => (φ (n+1))) := by
      ext n; rw [φ₁_equ fullrank₁ fullrank₂ n]; simp
   simp at this; rw [this]
   apply StrictMono.comp
   · apply hphi_StrictMono
   · simp [StrictMono]

-- The difference between this lemma and the one above is the change of sub-script.
-- A₂ (x₂ (φ₁ n) - x₂ ((φ₁ n) - 1)) → 0
lemma sub_Seq_converge_zero₃' [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => A₂ (x₂ (φ₁ n) - x₂ ((φ₁ n) - 1))) atTop (𝓝 0) := by
   apply Filter.tendsto_iff_seq_tendsto.1 Seq_converge_zero₃
   apply StrictMono.tendsto_atTop
   simp; rw [StrictMono]; intro n₁ n₂ h
   have h₁: φ (n₁ + 1) < φ (n₂ + 1) := by apply hphi_StrictMono; linarith
   have hn₁: φ (n₁ + 1) ≥ 1 := by
      calc
         _ ≥ n₁ + 1 := by apply StrictMono.id_le (hphi_StrictMono fullrank₁ fullrank₂)
         _ ≥ 1 := by linarith
   apply Nat.sub_lt_sub_right hn₁ h₁

-- (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n))) → 0
lemma const_smul_subseq₁ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n)))) atTop (𝓝 0) := by
   rw [← smul_zero (( 1 - τ) * ρ )]
   apply Filter.Tendsto.const_smul (sub_Seq_converge_zero₁ fullrank₁ fullrank₂) (( 1 - τ) * ρ)

-- ρ • A₂ (x₂ ((φ₁ n) - 1) - x₂ (φ₁ n)) → 0
lemma const_smul_subseq₂ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => ρ • A₂ (x₂ ((φ₁ n) - 1) - x₂ (φ₁ n))) atTop (𝓝 0) := by
   have : (fun n => ρ • A₂ (x₂ ((φ₁ n) - 1) - x₂ (φ₁ n))) = (fun n => (-ρ) • A₂ (x₂ (φ₁ n) - x₂ ((φ₁ n) - 1))) := by
      ext n
      calc
         _ = ρ • (-1) • A₂ (x₂ (φ₁ n) - x₂ ((φ₁ n) - 1)) := by simp
         _ = (-ρ) • A₂ (x₂ (φ₁ n) - x₂ ((φ₁ n) - 1)) := by
            rw [smul_comm, neg_one_smul]; simp
   rw [this, ← smul_zero (-ρ)]
   apply Filter.Tendsto.const_smul (sub_Seq_converge_zero₃' fullrank₁ fullrank₂)

-- u (φ₁ n) converges to (- A₁† y'')
lemma u_subseq_converge [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => u (φ₁ n)) atTop (𝓝 (- A₁† y'')) := by
   have : (fun n => u (φ₁ n)) = (fun n => - A₁† ((y (φ₁ n)) + (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n))
         + A₂ (e₂ (φ₁ n))) + ρ • (A₂ (x₂ ((φ₁ n) - 1) - x₂ (φ₁ n))))) := by
      funext n; rw [u]
   rw [this]
   have : Tendsto (fun n => (y (φ₁ n)) + (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n))
         + A₂ (e₂ (φ₁ n)))) atTop (𝓝 y'') := by
      rw [← add_zero y'']
      apply Filter.Tendsto.add (y_subseq_converge' fullrank₁ fullrank₂) (const_smul_subseq₁ fullrank₁ fullrank₂)
   have h: Tendsto (fun n => (y (φ₁ n)) + (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n))
         + A₂ (e₂ (φ₁ n))) + ρ • (A₂ (x₂ ((φ₁ n) - 1) - x₂ (φ₁ n)))) atTop (𝓝 y'') := by
      rw [← add_zero y'']
      apply Filter.Tendsto.add (this) (const_smul_subseq₂ fullrank₁ fullrank₂)
   have : Tendsto (- A₁†) (𝓝 y'') (𝓝 (- A₁† y'')) := by apply Continuous.tendsto; apply ContinuousLinearMap.continuous
   apply Filter.tendsto_iff_seq_tendsto.1 this; apply h

-- v (φ₁ n) converges to (- A₂† y'')
lemma v_subseq_converge [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n => v (φ₁ n)) atTop (𝓝 (- A₂† y'')) := by
   have : (fun n => v (φ₁ n)) = (fun n => - A₂† (y (φ₁ n) + (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n))))) := by
      funext n; rw [v]
   rw [this]
   have h: Tendsto (fun n => (y (φ₁ n) + (( 1 - τ) * ρ ) • (A₁ (e₁ (φ₁ n)) + A₂ (e₂ (φ₁ n))))) atTop (𝓝  y'') := by
      rw [← add_zero y'']
      apply Filter.Tendsto.add (y_subseq_converge' fullrank₁ fullrank₂) (const_smul_subseq₁ fullrank₁ fullrank₂)
   have : Tendsto (- A₂†) (𝓝 y'') (𝓝 (- A₂† y'')) := by apply Continuous.tendsto; apply ContinuousLinearMap.continuous
   apply Filter.tendsto_iff_seq_tendsto.1 this; apply h

-- (nonempty : ∀ (n : ℕ), g n ∈ SubderivAt f (x n)) (lscf : LowerSemicontinuous f)
-- (x_converge : Tendsto x atTop (𝓝 x')) (g_converge : Tendsto g atTop (𝓝 g'))

lemma A₁'y_inthesubgradient [Setting E₁ E₂ F admm admm_kkt] : - A₁† y'' ∈ SubderivAt f₁ x₁'':=
   Image_subgradient_closed (fun n ↦ u_inthesubgradient (φ₁ n)) admm.lscf₁
   (x₁_subseq_converge' fullrank₁ fullrank₂) (u_subseq_converge   fullrank₁ fullrank₂)

lemma A₂'y_inthesubgradient [Setting E₁ E₂ F admm admm_kkt]  : - A₂† y'' ∈ SubderivAt f₂ x₂'':=
   Image_subgradient_closed (fun n => v_inthesubgradient (φ₁ n)) admm.lscf₂
   (x₂_subseq_converge' fullrank₁ fullrank₂) (v_subseq_converge   fullrank₁ fullrank₂)

-- lim ‖ x_n ‖ = ‖ lim x_n ‖
lemma Satisfying_equational_constraint1' [Setting E₁ E₂ F admm admm_kkt] : Tendsto A₁ (𝓝 x₁'') (𝓝 (A₁ x₁'')) := by
   apply Continuous.tendsto
   apply ContinuousLinearMap.continuous

lemma Satisfying_equational_constraint1 [Setting E₁ E₂ F admm admm_kkt] :
Tendsto (fun n => A₁ (x₁ (φ n))) atTop (𝓝 (A₁ x₁'')) := by
   apply tendsto_iff_seq_tendsto.1 (Satisfying_equational_constraint1' fullrank₁ fullrank₂) (x₁ ∘ φ)
   apply tendsto_iff_seq_tendsto.1 (x₁_subseq_converge fullrank₁ fullrank₂)
   apply StrictMono.tendsto_atTop
   apply strictMono_id

lemma Satisfying_equational_constraint2' [Setting E₁ E₂ F admm admm_kkt] : Tendsto A₂ (𝓝 x₂'') (𝓝 (A₂ x₂'')) := by
   apply Continuous.tendsto
   apply ContinuousLinearMap.continuous

lemma Satisfying_equational_constraint2 [Setting E₁ E₂ F admm admm_kkt] :
Tendsto (fun n => A₂ (x₂ (φ n))) atTop (𝓝 (A₂ x₂'')) := by
   apply tendsto_iff_seq_tendsto.1 (Satisfying_equational_constraint2' fullrank₁ fullrank₂) (x₂ ∘ φ)
   apply tendsto_iff_seq_tendsto.1 (x₂_subseq_converge fullrank₁ fullrank₂)
   apply StrictMono.tendsto_atTop
   apply strictMono_id

lemma Satisfying_equational_constraint' [Setting E₁ E₂ F admm admm_kkt] :
Tendsto (fun n => ‖A₁ (x₁ (φ n)) + A₂ (x₂ (φ n)) - b‖) atTop (𝓝 ‖(A₁ x₁'') + (A₂ x₂'') - admm.b‖)
:= by
   apply Tendsto.norm
   apply Tendsto.sub_const
   apply Tendsto.add
   apply Satisfying_equational_constraint1
   apply Satisfying_equational_constraint2

lemma subconverge_zero₂ [Setting E₁ E₂ F admm admm_kkt] : Tendsto (fun n =>  ‖A₁ (x₁ (φ n)) + A₂ (x₂ (φ n)) - b‖)  atTop (𝓝 0)
:= by
   apply tendsto_iff_seq_tendsto.1 converge_zero₂
   apply StrictMono.tendsto_atTop
   apply hphi_StrictMono

lemma Satisfying_equational_constraint_norm [Setting E₁ E₂ F admm admm_kkt] :
      ‖(A₁ x₁'') + (A₂ x₂'') - admm.b‖ = 0 := by
   apply tendsto_nhds_unique (Satisfying_equational_constraint' fullrank₁ fullrank₂)
   apply subconverge_zero₂

lemma Satisfying_equational_constraint [Setting E₁ E₂ F admm admm_kkt] :
      (A₁ x₁'') + (A₂ x₂'') = admm.b := by
   have h1 := Satisfying_equational_constraint_norm fullrank₁ fullrank₂
   apply norm_eq_zero.1 at h1
   apply eq_of_sub_eq_zero h1

lemma Iskktpair [Setting E₁ E₂ F admm admm_kkt] : Convex_KKT x₁'' x₂'' y'' admm.toOptProblem :=
   {
      subgrad₁ :=A₁'y_inthesubgradient fullrank₁ fullrank₂
      subgrad₂ :=A₂'y_inthesubgradient fullrank₁ fullrank₂
      eq       :=Satisfying_equational_constraint fullrank₁ fullrank₂
   }

end

variable (fullrank₁: Function.Injective admm.A₁) (fullrank₂: Function.Injective admm.A₂)
-- Subsequence mapping
local notation "φ" => Converge_Subseq.φ (Subseq fullrank₁ fullrank₂)

-- The point of the subsequence convergence
local notation "x₁''" => Converge_Subseq.x₁'' (Subseq fullrank₁ fullrank₂)
local notation "x₂''" => Converge_Subseq.x₂'' (Subseq fullrank₁ fullrank₂)
local notation "y''"  => Converge_Subseq.y'' (Subseq fullrank₁ fullrank₂)

def admm_kkt₁ [_s : Setting E₁ E₂ F admm admm_kkt] :  Existance_of_kkt admm :=
   Existance_of_kkt.mk x₁''  x₂''  y'' (Iskktpair fullrank₁ fullrank₂)

-- e₁ (φ n) → 0
-- x₁ (φ n) → (admm_kkt₁ fullrank₁ fullrank₂).x₁ = x₁''
lemma e₁_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (e₁ ∘ φ) atTop (𝓝 0) := by
   have h₁: Tendsto (fun n => (x₁ ∘ φ) n - x₁'') atTop (𝓝 0) := by
      apply tendsto_sub_nhds_zero_iff.2; apply x₁_subseq_converge
   have h₂: (fun n => (x₁ ∘ φ) n - x₁'') = (fun n => e₁ (φ n)) := by
      funext n; rw [e₁]; simp; simp [admm_kkt₁]; rfl
   rw [h₂] at h₁; apply h₁

-- e₂ (φ n) → 0
-- x₂ (φ n) → (admm_kkt₁ fullrank₁ fullrank₂).x₂ = x₂''
lemma e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (e₂ ∘ φ) atTop (𝓝 0) := by
   have h₁: Tendsto (fun n => (x₂ ∘ φ) n - x₂'') atTop (𝓝 0) := by
      apply tendsto_sub_nhds_zero_iff.2; apply x₂_subseq_converge
   have h₂: (fun n => (x₂ ∘ φ) n - x₂'') = (fun n => e₂ (φ n)) := by
      funext n; rw [e₂]; simp; simp [admm_kkt₁]; rfl
   rw [h₂] at h₁; apply h₁

-- e₂ (φ n) → 0
-- y (φ n) → (admm_kkt₁ fullrank₁ fullrank₂).y = y''
lemma ey_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (ey ∘ φ) atTop (𝓝 0) := by
   have h₁: Tendsto (fun n => (y ∘ φ) n - y'') atTop (𝓝 0) := by
      apply tendsto_sub_nhds_zero_iff.2; apply y_subseq_converge
   have h₂: (fun n => (y ∘ φ) n - y'') = (fun n => ey (φ n)) := by
      funext n; rw [ey]; simp; simp [admm_kkt₁]; rfl
   rw [h₂] at h₁; apply h₁

-- ‖ey (φ n)‖ → 0
lemma nrm_ey_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖ey (φ n)‖) atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.1; apply ey_subseq_converge_zero

-- ‖ey (φ n)‖^2 → 0
lemma sqnrm_ey_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖ey (φ n)‖^2) atTop (𝓝 0) := by
   rw [← zero_pow]; apply Filter.Tendsto.pow ; apply nrm_ey_subseq_converge_zero; linarith

-- (1 / (τ * ρ)) * ‖ey (φ n)‖^2 → 0
lemma const_sqnrm_ey_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => (1 / (τ * ρ)) * ‖ey (φ n)‖^2) atTop (𝓝 0) := by
   rw [← mul_zero]
   apply Filter.Tendsto.const_mul (1 / (τ * ρ)) (sqnrm_ey_subseq_converge_zero fullrank₁ fullrank₂)

-- A₁ (e₁ (φ n)) → 0
lemma A₁e₁_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => A₁ (e₁ (φ n))) atTop (𝓝 0) := by
   have h₁: Tendsto A₁ (𝓝 0) (𝓝 (A₁ 0)) := by
      apply Continuous.tendsto; apply ContinuousLinearMap.continuous
   simp at h₁; apply Filter.tendsto_iff_seq_tendsto.1 h₁; apply e₁_subseq_converge_zero

-- A₂ (e₂ (φ n)) → 0
lemma A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => A₂ (e₂ (φ n))) atTop (𝓝 0) := by
   have h₁: Tendsto A₂ (𝓝 0) (𝓝 (A₂ 0)) := by
      apply Continuous.tendsto; apply ContinuousLinearMap.continuous
   simp at h₁; apply Filter.tendsto_iff_seq_tendsto.1 h₁; apply e₂_subseq_converge_zero

-- ‖A₂ (e₂ (φ n))‖ → 0
lemma nrm_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₂ (e₂ (φ n))‖) atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.1; apply A₂e₂_subseq_converge_zero

-- ‖A₂ (e₂ (φ n))‖^2 → 0
lemma sqnrm_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
   rw [← zero_pow]; apply Filter.Tendsto.pow ; apply nrm_A₂e₂_subseq_converge_zero; linarith

-- ρ * ‖A₂ (e₂ (φ n))‖^2 → 0
lemma const_sqnrm_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ρ * ‖A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
   rw [← mul_zero]
   apply Filter.Tendsto.const_mul ρ (sqnrm_A₂e₂_subseq_converge_zero fullrank₁ fullrank₂)

-- A₁ (e₁ (φ n)) + A₂ (e₂ (φ n)) → 0
lemma A₁e₁_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))) atTop (𝓝 0) := by
   rw [← add_zero 0]
   apply Tendsto.add (A₁e₁_subseq_converge_zero fullrank₁ fullrank₂) (A₂e₂_subseq_converge_zero fullrank₁ fullrank₂)

-- ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖ → 0
lemma nrm_A₁e₁_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖) atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.1; apply A₁e₁_A₂e₂_subseq_converge_zero

-- ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2 → 0
lemma sqnrm_A₁e₁_A₂e₂_subseq_converge_zero[Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
   rw [← zero_pow]; apply Filter.Tendsto.pow ; apply nrm_A₁e₁_A₂e₂_subseq_converge_zero; linarith

-- ((max (1-τ) (1-(1/τ)))*ρ) * ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2 → 0
lemma const_sqnrm_A₁e₁_A₂e₂_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ((max (1-τ) (1-(1/τ)))*ρ) * ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
   rw [← mul_zero]
   apply Filter.Tendsto.const_mul ((max (1-τ) (1-(1/τ)))*ρ) (sqnrm_A₁e₁_A₂e₂_subseq_converge_zero fullrank₁ fullrank₂)

-- Φ (φ n) → 0
lemma Φ_subseq_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => Φ (φ n)) atTop (𝓝 0) := by
   have h_add: Tendsto (fun n => (1 / (τ * ρ)) * ‖ey (φ n)‖^2 + ρ * ‖A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
      rw [← zero_add 0]
      apply Tendsto.add (const_sqnrm_ey_subseq_converge_zero fullrank₁ fullrank₂) (const_sqnrm_A₂e₂_subseq_converge_zero fullrank₁ fullrank₂)
   have h_add': Tendsto (fun n => (1 / (τ * ρ)) * ‖ey (φ n)‖^2 + ρ * ‖A₂ (e₂ (φ n))‖^2 + ((max (1-τ) (1-(1/τ)))*ρ) * ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2) atTop (𝓝 0) := by
      rw [← zero_add 0]
      apply Tendsto.add h_add (const_sqnrm_A₁e₁_A₂e₂_subseq_converge_zero fullrank₁ fullrank₂)
   have : (fun n => Φ (φ n)) = (fun n => (1 / (τ * ρ)) * ‖ey (φ n)‖^2 + ρ * ‖A₂ (e₂ (φ n))‖^2 + ((max (1-τ) (1-(1/τ)))*ρ) * ‖A₁ (e₁ (φ n)) + A₂ (e₂ (φ n))‖^2) := by
      funext n; rw [Φ, Ψ]
   rw [this]
   apply h_add'

lemma Φ_ge [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      ∀ n , 0 ≤ (fun _ : ℕ ↦ (⨅ i, (fun n ↦ Φ (n + 1)) i)) n := by
   intro n
   simp only
   apply Real.iInf_nonneg (f := (fun n ↦ Φ (n + 1)))
   intro i
   apply Φ_is_nonneg (i+1)

lemma Φ_bddbelow [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      BddBelow (range (fun n ↦ Φ (n + 1))) := by
   simp [BddBelow , lowerBounds]
   use 0
   simp only [mem_setOf_eq]
   intro a
   apply Φ_is_nonneg (a+1)

lemma Φ_le [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:∀ n : ℕ , (⨅ i, (fun n ↦ Φ (n + 1)) i) ≤ Φ (φ n.succ) := by
   intro n
   have := ciInf_le (Φ_bddbelow fullrank₁ fullrank₂) ((φ n.succ)-1)
   have h : φ n.succ > 0:= by
      calc _
         _ ≥ n + 1  := StrictMono.id_le (hphi_StrictMono fullrank₁ fullrank₂) (n + 1)
         _ > 0      :=by linarith
   have h2 : 1 ≤ φ n.succ := by linarith[h]
   have h1 : φ n.succ - 1 + 1 = φ n.succ := by apply Nat.sub_add_cancel h2
   rw[h1] at this
   exact this

lemma Φ_converge_zero''' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
 Tendsto (fun _ : ℕ ↦ (⨅ i, (fun n ↦ Φ (n + 1)) i)) atTop (𝓝 0) := by
   apply squeeze_zero
   apply Φ_ge
   apply Φ_le
   have :=Φ_subseq_converge_zero fullrank₁ fullrank₂
   rw[← tendsto_add_atTop_iff_nat 1] at this
   exact this

lemma Φ_converge_zero'' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
 Tendsto (fun _ : ℕ ↦ (⨅ i, (fun n ↦ Φ (n + 1)) i)) atTop (𝓝 (⨅ i, (fun n ↦ Φ (n + 1)) i)) := by
 apply tendsto_const_nhds

lemma Φ_converge_zero' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      (⨅ i, (fun n ↦ Φ (n + 1)) i) = 0  := by
   apply tendsto_nhds_unique (Φ_converge_zero'' fullrank₁ fullrank₂)
   apply Φ_converge_zero'''

lemma Φ_isMono [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Antitone (fun n ↦ Φ (n + 1)) := by
   apply antitone_nat_of_succ_le
   intro n
   apply Φ_is_monotone (n+1).toPNat'

lemma Φ_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto Φ atTop (𝓝 0) := by
   rw[← tendsto_add_atTop_iff_nat 1]
   have := tendsto_atTop_ciInf (Φ_isMono fullrank₁ fullrank₂) (Φ_bddbelow fullrank₁ fullrank₂)
   rwa[← Φ_converge_zero']

lemma A₂e₂_le_Φ (n : ℕ) [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      ‖A₂ (e₂ n)‖ ^ 2 ≤ (1 / ρ) * Φ n := by
   have hτ : τ > 0 := by rcases admm.htau with ⟨h₁, _⟩; exact h₁
   have hτ' : τ ≥ 0 := by apply le_of_lt hτ
   have h1 (n : ℕ) : (1 / ρ) * Φ n = ρ⁻¹ * Φ n := by simp only [one_div]
   have open_Φ (n : ℕ) : ρ⁻¹ * Φ n = ((ρ⁻¹) ^ 2) * τ⁻¹ * ‖ey n‖^2 + ‖A₂ (e₂ n)‖ ^ 2 + (max (1 - τ) (1 - 1 / τ)) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 := by
      simp [Φ, Ψ]; ring_nf; rw [mul_inv_cancel₀, one_mul, one_mul]; ring_nf; apply ne_of_gt (admm.hrho)
   have open_Φ' (n : ℕ) : ((ρ⁻¹) ^ 2) * τ⁻¹ * ‖ey n‖^2 + ‖A₂ (e₂ n)‖ ^ 2 + (max (1 - τ) (1 - 1 / τ)) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 = ‖A₂ (e₂ n)‖ ^ 2 + (((ρ⁻¹) ^ 2) * τ⁻¹ * ‖ey n‖^2 + (max (1 - τ) (1 - 1 / τ)) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2) := by
      ring_nf
   have nonneg1 (n : ℕ) : ((ρ⁻¹) ^ 2) * τ⁻¹ * ‖ey n‖^2 ≥ 0 := by
      have h₁ : (ρ⁻¹) ^ 2 ≥ 0 := by apply pow_two_nonneg
      have h₂ : τ⁻¹ ≥ 0 := by apply inv_nonneg.mpr hτ'
      have h₃ : ‖ey n‖^2 ≥ 0 := by apply pow_two_nonneg
      apply mul_nonneg (mul_nonneg h₁ h₂) h₃
   have nonneg2 (n : ℕ) : (max (1 - τ) (1 - 1 / τ)) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 ≥ 0:= by
      have h3 : (max (1 - τ) (1 - 1 / τ)) ≥ 0 := by apply nonneg₃
      apply mul_nonneg h3
      apply pow_two_nonneg
   have nonneg3 (n : ℕ) : ((ρ⁻¹) ^ 2) * τ⁻¹ * ‖ey n‖^2 + (max (1 - τ) (1 - 1 / τ)) * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 ≥ 0 := by
      apply add_nonneg (nonneg1 n) (nonneg2 n)
   rw [h1, open_Φ, open_Φ']; linarith [nonneg3 n]

lemma A₂e₂_le_Φ' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))](n : ℕ) :
      ‖‖A₂ (e₂ n)‖ ^ 2‖ ≤ (1 / ρ) * Φ n := by
   have : ‖‖A₂ (e₂ n)‖ ^ 2‖ = ‖A₂ (e₂ n)‖ ^ 2 := by simp only [norm_pow, norm_norm]
   rw [this]
   apply A₂e₂_le_Φ

lemma A₂e₂_pow_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₂ (e₂ n)‖^2) atTop (𝓝 0) := by
   apply squeeze_zero_norm; apply A₂e₂_le_Φ'
   have h1 : Tendsto (fun n ↦ (1 / ρ) * Φ n) atTop (𝓝 (1 / ρ * 0)) := by
      apply Filter.Tendsto.const_mul (1 / ρ) (Φ_converge_zero fullrank₁ fullrank₂)
   have h2 : Tendsto (fun n ↦ (1 / ρ) * Φ n) atTop (𝓝 0) := by
      have : 1 / ρ * 0 = 0 := by norm_num
      rw [← this]
      exact h1
   assumption

lemma A₂e₂_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₂ (e₂ n)‖) atTop (𝓝 0) := by
   have : Tendsto (fun n => √((‖A₂ (e₂ n)‖)^2))  atTop (𝓝 √0) := by
      apply Tendsto.sqrt (A₂e₂_pow_converge_zero fullrank₁ fullrank₂)
   rw [Real.sqrt_zero] at this; simp [Real.sqrt_sq] at this; exact this

lemma A₁e₁_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖A₁ (e₁ n)‖) atTop (𝓝 0) := by
   have h (n : ℕ) : ‖A₁ (e₁ n)‖ ≤ ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖ := by
      let x := A₁ (e₁ n)
      let xx := A₂ (e₂ n)
      have h1 : ‖x‖ = ‖x + xx - xx‖ := by rw [← add_sub, sub_self, add_zero]
      have h2 : ‖x + xx - xx‖ ≤ ‖x + xx‖ + ‖xx‖ := by apply norm_sub_le
      rw [← h1] at h2
      linarith
   have h' (n : ℕ) : ‖‖A₁ (e₁ n)‖‖ ≤ ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖ := by
      have : ‖‖A₁ (e₁ n)‖‖ = ‖A₁ (e₁ n)‖ := by simp only [norm_norm]
      rw [this]
      exact h n
   have h'' : Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖) atTop (𝓝 (0 + 0)) := by
      apply Tendsto.add (converge_zero₁) (A₂e₂_converge_zero fullrank₁ fullrank₂)
   have h''' : Tendsto (fun n => ‖A₁ (e₁ n) + A₂ (e₂ n)‖ + ‖A₂ (e₂ n)‖) atTop (𝓝 0) := by
      have : (0 : ℝ) = 0 + 0 := by norm_num
      rw [this]
      exact h''
   apply squeeze_zero_norm
   apply h'
   exact h'''

lemma A₁e₁_converge_zero' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖(A₁ ∘ e₁) n‖) atTop (𝓝 0) := by
   have : (fun n => ‖A₁ (e₁ n)‖) = (fun n => ‖(A₁ ∘ e₁) n‖) := by simp only [Function.comp_apply]
   rw [← this]
   apply A₁e₁_converge_zero

lemma CA₁e₁_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))](C : ℝ) :
      Tendsto (fun n => C * ‖A₁ (e₁ n)‖) atTop (𝓝 0) := by
   have : Tendsto (fun n => ‖A₁ (e₁ n)‖) atTop (𝓝 0) := by apply A₁e₁_converge_zero
   have h : C * 0 = 0 := by simp only [mul_zero]
   rw[← h]; apply Tendsto.const_mul C this

lemma CA₂e₂_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))](C : ℝ) :
      Tendsto (fun n => C * ‖A₂ (e₂ n)‖) atTop (𝓝 0) := by
   have : Tendsto (fun n => ‖A₂ (e₂ n)‖) atTop (𝓝 0) := by apply A₂e₂_converge_zero
   have h : C * 0 = 0 := by simp only [mul_zero]
   rw[← h]; apply Tendsto.const_mul C this

lemma e₁_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto e₁ atTop (𝓝 0) := by
   have : ∃ C > 0, ∀ n : ℕ, ‖e₁ n‖ ≤ C * ‖A₁ (e₁ n)‖ := open_mapping_e₁ fullrank₁
   obtain ⟨C, _, hC⟩ := this
   apply squeeze_zero_norm; intro n; exact hC n; apply CA₁e₁_converge_zero

lemma e₂_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto e₂ atTop (𝓝 0) := by
   have : ∃ C > 0, ∀ n : ℕ, ‖e₂ n‖ ≤ C * ‖A₂ (e₂ n)‖ := open_mapping_e₂ fullrank₂
   obtain ⟨C, _, hC⟩ := this
   apply squeeze_zero_norm; intro n; exact hC n; apply CA₂e₂_converge_zero

lemma ey_le_Φ [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))](n : ℕ) :
      (1 / (τ * ρ)) * ‖ey n‖ ^ 2 ≤ Φ n := by
   dsimp [Φ, Ψ]
   have h : ρ * ‖A₂ (e₂ n)‖ ^ 2 ≥ 0 := by
      apply mul_nonneg
      linarith [admm.hrho]
      linarith [pow_two_nonneg (‖A₂ (e₂ n)‖)]
   have h' : max (1 - τ) (1 - 1 / τ) * ρ * ‖A₁ (e₁ n) + A₂ (e₂ n)‖ ^ 2 ≥ 0 := by
      apply mul_nonneg
      apply mul_nonneg
      linarith [nonneg₃, admm.hrho]
      linarith [admm.hrho]
      linarith [pow_two_nonneg (‖A₁ (e₁ n) + A₂ (e₂ n)‖)]
   linarith [h, h']

lemma ey_le_Φ' [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))] (n : ℕ) :
      ‖ey n‖ ^ 2 ≤ (τ * ρ) * Φ n := by
   have : (τ * ρ) * Φ n = Φ n * (τ * ρ) := by ring
   rw [this]
   have : (τ * ρ) > 0 := by apply mul_pos; linarith [admm.htau.1]; linarith [admm.hrho]
   apply (div_le_iff₀ this).mp
   calc
      _= (1 / (τ * ρ)) * ‖ey n‖ ^ 2 := by ring
      _≤ Φ n := by apply ey_le_Φ

lemma const_φ_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => (τ * ρ) * Φ n) atTop (𝓝 0) := by
   rw [← mul_zero (τ * ρ)]
   apply Filter.Tendsto.const_mul (τ * ρ) (Φ_converge_zero fullrank₁ fullrank₂)

lemma ey_sqnrm_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖ey n‖^2)  atTop (𝓝 0) := by
   apply squeeze_zero_norm
   have (n : ℕ) : ‖‖ey n‖ ^ 2‖ ≤ (τ * ρ) * Φ n := by simp [ey_le_Φ']
   apply this; apply const_φ_converge_zero

lemma ey_nrm_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto (fun n => ‖ey n‖)  atTop (𝓝 0) := by
   rw [← Real.sqrt_zero]
   have : (fun n => ‖ey n‖) = (fun n => √(‖ey n‖^2)) := by funext n; simp [Real.sqrt_sq]
   rw [this]
   apply Filter.Tendsto.sqrt (ey_sqnrm_converge_zero fullrank₁ fullrank₂)

lemma ey_converge_zero [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto ey atTop (𝓝 0) := by
   apply tendsto_zero_iff_norm_tendsto_zero.2
   apply ey_nrm_converge_zero

--lim_{ n → ∞} x_n - x = 0 =>  lim_{ n → ∞} x_n  = x
lemma x₁_converge [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto x₁ atTop (𝓝 x₁'') := by
   have : e₁ = (fun n => (x₁ n) - x₁''):= rfl
   have h := e₁_converge_zero fullrank₁ fullrank₂
   rw[this , tendsto_sub_nhds_zero_iff] at h
   exact h

lemma x₂_converge [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto x₂ atTop (𝓝 x₂'') := by
   have : e₂ = (fun n => (x₂ n) - x₂''):= rfl
   have h := e₂_converge_zero fullrank₁ fullrank₂
   rw[this , tendsto_sub_nhds_zero_iff] at h
   exact h

lemma y_converge [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      Tendsto y atTop (𝓝 y'') := by
   have : ey = (fun n => (y n) - y''):= rfl
   have h := ey_converge_zero fullrank₁ fullrank₂
   rw[this , tendsto_sub_nhds_zero_iff] at h
   exact h

--ADMM收敛定理
theorem ADMM_convergence [Setting E₁ E₂ F admm (admm_kkt₁ fullrank₁ fullrank₂ (admm_kkt := admm_kkt) (_s := ⟨⟩))]:
      ∃ ( _x₁   : E₁) ( _x₂ : E₂) ( _y : F) , Convex_KKT _x₁ _x₂ _y admm.toOptProblem
      ∧ ( Tendsto x₁ atTop (𝓝 _x₁)∧ Tendsto x₂ atTop (𝓝 _x₂)∧ Tendsto y atTop (𝓝 _y)) :=
   ⟨x₁'',x₂'',y'',Iskktpair fullrank₁ fullrank₂ ,
   x₁_converge fullrank₁ fullrank₂ ,x₂_converge fullrank₁ fullrank₂,
   y_converge fullrank₁ fullrank₂⟩

end ADMM_Converge_Proof
