Discovery.Linear­Disentanglement.Quantitative.Pairwise­Affine

theorem pairwiseResidualRadius_pos {p : ℕ} {M δ L : ℝ} (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) : 0 < pairwiseResidualRadius p M δ L := by unfold pairwiseResidualRadius positivity

theorem pairwiseLocalRadius_pos {p : ℕ} {M δ L J : ℝ} (hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hJ : 0 < J) : 0 < pairwiseLocalRadius p M δ L J := by unfold pairwiseLocalRadius positivity

theorem one_le_conditionRoot {p : ℕ} {κ : ℝ} (hp : 0 < p) (hκ : 1 ≤ κ) : 1 ≤ conditionRoot p κ := by unfold conditionRoot apply Real.one_le_rpow · have hf : (1 : ℝ) ≤ factorial p := by exact_mod_cast Nat.factorial_pos p have hk : (1 : ℝ) ≤ κ ^ (p - 1) := one_le_pow₀ hκ nlinarith · positivity

theorem pairMatrixNormBound_conditionRoot {p : ℕ} {κ : ℝ} (B₀ B : SqMatrix p) (hp : 0 < p) (hκ : 1 ≤ κ) (henv : PairDetConditionEnvelope κ B₀ B) : PairMatrixNormBound (conditionRoot p κ) B₀ B := by exact ⟨opNorm_le_conditionRoot B₀ hp hκ henv.1, opNorm_le_conditionRoot B hp hκ henv.2⟩

theorem entryL2_le_dimension_mul_opNorm {p : ℕ} (X : SqMatrix p) (hp : 0 < p) : entryL2 X ≤ (p : ℝ) * ‖X‖ := by rw [entryL2_eq_sqrt, Real.sqrt_le_iff] constructor · positivity · calc ∑ i, ∑ j, |X i j| ^ 2 ≤ ∑ _i : Fin p, ∑ _j : Fin p, ‖X‖ ^ 2 := by gcongr with i j exact abs_entry_le_opNorm X i j _ = ((p : ℝ) * ‖X‖) ^ 2 := by simp [Finset.sum_const, nsmul_eq_mul] ring

theorem transitionError_eq_sub_mul_inv {p : ℕ} (B₀ B : SqMatrix p) (hunit : IsUnit B₀.det) : transitionError B₀ B = (B - B₀) * B₀⁻¹ := by unfold transitionError transition rw [Matrix.sub_mul, Matrix.mul_nonsing_inv B₀ hunit]

theorem transitionError_entryL2_le_of_neighborhood {p : ℕ} (B₀ B : SqMatrix p) {J ρ : ℝ} (hp : 0 < p) (hJ : 0 ≤ J) (hunit : IsUnit B₀.det) (hinv : ‖B₀⁻¹‖ ≤ J) (hlocal : InReferenceNeighborhood ρ B₀ B) : entryL2 (transitionError B₀ B) ≤ (p : ℝ) * J * ρ := by rw [transitionError_eq_sub_mul_inv B₀ B hunit] calc entryL2 ((B - B₀) * B₀⁻¹) ≤ entryL2 (B - B₀) * entryL2 B₀⁻¹ := entryL2_mul_le _ _ _ ≤ ρ * ((p : ℝ) * J) := by have hρ : 0 ≤ ρ := (entryL2_nonneg _).trans hlocal apply mul_le_mul hlocal · exact (entryL2_le_dimension_mul_opNorm B₀⁻¹ hp).trans (mul_le_mul_of_nonneg_left hinv (by positivity)) · exact entryL2_nonneg _ · exact hρ _ = (p : ℝ) * J * ρ := by ring

theorem invOpNorm_le_conditionEnvelope {p : ℕ} {κ : ℝ} (B : SqMatrix p) (hp : 0 < p) (hdiag : UnitDiagonal B) (henv : DetConditionEnvelope κ B) : ‖B⁻¹‖ ≤ κ := by letI : Nonempty (Fin p) := Fin.pos_iff_nonempty.mp hp let i : Fin p := choice (inferInstance : Nonempty (Fin p)) have hB : 1 ≤ ‖B‖ := by simpa [hdiag i] using abs_entry_le_opNorm B i i calc ‖B⁻¹‖ ≤ ‖B‖ * ‖B⁻¹‖ := by nlinarith [norm_nonneg B⁻¹] _ = operatorConditionNumber B := rfl _ ≤ κ := henv.2.2

-- Proof route: `|s₁ k-s₀ k| ≤ 2M`, then Cauchy--Schwarz on the two rows and the -- fact that each row's squared sum is bounded by the full entrywise squared sum. theorem coordinateProductRemainder_le {p : ℕ} {E : Type*} [Fintype E] (s : E → Fin p → ℝ) (R : SqMatrix p) {M : ℝ} (hM : 0 ≤ M) (hscale : ShiftScaleBound s M) (e₁ e₀ : E) (i j : Fin p) : |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| ≤ 2 * M * entryL2 R ^ 2 := by classical have hshift (k : Fin p) : |s e₁ k - s e₀ k| ≤ 2 * M := by calc |s e₁ k - s e₀ k| ≤ |s e₁ k| + |s e₀ k| := abs_sub _ _ _ ≤ M + M := add_le_add (hscale _ _) (hscale _ _) _ = 2 * M := by ring have hterm (k : Fin p) : |R i k * R j k * (s e₁ k - s e₀ k)| ≤ M * (|R i k| ^ 2 + |R j k| ^ 2) := by have huv : 2 * (|R i k| * |R j k|) ≤ |R i k| ^ 2 + |R j k| ^ 2 := by nlinarith [sq_nonneg (|R i k| - |R j k|)] calc |R i k * R j k * (s e₁ k - s e₀ k)| = (|R i k| * |R j k|) * |s e₁ k - s e₀ k| := by simp only [abs_mul] _ ≤ (|R i k| * |R j k|) * (2 * M) := by gcongr exact hshift k _ ≤ M * (|R i k| ^ 2 + |R j k| ^ 2) := by nlinarith [mul_nonneg (abs_nonneg (R i k)) (abs_nonneg (R j k))] have hrow (a : Fin p) : (∑ k, |R a k| ^ 2) ≤ ∑ u, ∑ k, |R u k| ^ 2 := by exact Finset.single_le_sum (fun u _ => sum_nonneg fun k _ => sq_nonneg |R u k|) (Finset.mem_univ a) have hentry : entryL2 R ^ 2 = ∑ u, ∑ k, |R u k| ^ 2 := by rw [entryL2_eq_sqrt, Real.sq_sqrt] positivity calc |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| ≤ ∑ k, |R i k * R j k * (s e₁ k - s e₀ k)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ k, M * (|R i k| ^ 2 + |R j k| ^ 2) := by gcongr with k exact hterm k _ = M * ((∑ k, |R i k| ^ 2) + ∑ k, |R j k| ^ 2) := by simp_rw [mul_add] rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum] _ ≤ 2 * M * (∑ u, ∑ k, |R u k| ^ 2) := by nlinarith [hrow i, hrow j] _ = 2 * M * entryL2 R ^ 2 := by rw [hentry]

theorem pair_cramer_control {a b c d x y r₁ r₂ M δ η : ℝ} (hM : 0 ≤ M) (hδ : 0 < δ) (hη : 0 ≤ η) (hcoeff : |a| ≤ 2 * M ∧ |b| ≤ 2 * M ∧ |c| ≤ 2 * M ∧ |d| ≤ 2 * M) (hdet : δ ≤ |a * d - c * b|) (heq₁ : a * x + b * y = r₁) (heq₂ : c * x + d * y = r₂) (hr₁ : |r₁| ≤ η) (hr₂ : |r₂| ≤ η) : |x| ≤ pairwiseSolveFactor M δ * η ∧ |y| ≤ pairwiseSolveFactor M δ * η := by have hxid : (a * d - c * b) * x = d * r₁ - b * r₂ := by rw [← heq₁, ← heq₂] ring_nf have hyid : (a * d - c * b) * y = a * r₂ - c * r₁ := by rw [← heq₁, ← heq₂] ring have hxnum : |d * r₁ - b * r₂| ≤ 4 * M * η := by calc |d * r₁ - b * r₂| ≤ |d * r₁| + |b * r₂| := abs_sub _ _ _ = |d| * |r₁| + |b| * |r₂| := by simp only [abs_mul] _ ≤ (2 * M) * η + (2 * M) * η := by exact add_le_add (mul_le_mul hcoeff.2.2.2 hr₁ (abs_nonneg r₁) (by positivity)) (mul_le_mul hcoeff.2.1 hr₂ (abs_nonneg r₂) (by positivity)) _ = 4 * M * η := by ring have hynum : |a * r₂ - c * r₁| ≤ 4 * M * η := by calc |a * r₂ - c * r₁| ≤ |a * r₂| + |c * r₁| := abs_sub _ _ _ = |a| * |r₂| + |c| * |r₁| := by simp only [abs_mul] _ ≤ (2 * M) * η + (2 * M) * η := by exact add_le_add (mul_le_mul hcoeff.1 hr₂ (abs_nonneg r₂) (by positivity)) (mul_le_mul hcoeff.2.2.1 hr₁ (abs_nonneg r₁) (by positivity)) _ = 4 * M * η := by ring have hxmul : δ * |x| ≤ 4 * M * η := by calc δ * |x| ≤ |a * d - c * b| * |x| := by gcongr _ = |d * r₁ - b * r₂| := by rw [← abs_mul, hxid] _ ≤ 4 * M * η := hxnum have hymul : δ * |y| ≤ 4 * M * η := by calc δ * |y| ≤ |a * d - c * b| * |y| := by gcongr _ = |a * r₂ - c * r₁| := by rw [← abs_mul, hyid] _ ≤ 4 * M * η := hynum constructor <;> unfold pairwiseSolveFactor <;> rw [div_mul_eq_mul_div] <;> apply (le_div_iff₀ hδ).2 <;> nlinarith [mul_nonneg hM hη]

-- Proof route: put `Q = B B₀⁻¹ = I+R`. Subtract the congruence equations at `e₀` -- from those at `e₁,e₂`. The `(i,j)` entries give a 2×2 system in `R i j` and -- `R j i`; `coordinateProductRemainder_le` bounds its nonlinear terms and the two -- off-diagonal residuals contribute `2ε`. Apply `pair_cramer_control`. theorem selectedTriple_offDiagonal_control {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ ε : ℝ} (i j : Fin p) (hij : i ≠ j) (e₀ e₁ e₂ : E) (hM : 0 ≤ M) (hδ : 0 < δ) (hε : 0 ≤ ε) (hscale : ShiftScaleBound s M) (hdet : δ ≤ |pairAffineDet s i j e₀ e₁ e₂|) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (happrox : OffDiagonalApproximateCongruence A B ε) : let R := transitionError B₀ B let η := 2 * M * entryL2 R ^ 2 + 2 * ε |R i j| ≤ pairwiseSolveFactor M δ * η ∧ |R j i| ≤ pairwiseSolveFactor M δ * η := by classical dsimp only let Q := transition B₀ B let R := transitionError B₀ B have hQR : Q = 1 + R := by ext u v simp [Q, R, transitionError, Matrix.sub_apply] have hformula (e : E) : (B * A e * B.transpose) i j = R i j * s e j + R j i * s e i + ∑ k, R i k * R j k * s e k := by rw [← transition_diagonal_congruence A s B₀ B hunit hexact e] have hentry : (Q * diagonal (s e) * Q.transpose) i j = ∑ k, Q i k * s e k * Q j k := by simp [Matrix.mul_apply, Matrix.diagonal_apply] change (Q * diagonal (s e) * Q.transpose) i j = _ rw [hentry, hQR] simp only [Matrix.add_apply, Matrix.one_apply] ring_nf repeat rw [Finset.sum_add_distrib] simp only [ite_mul, one_mul, zero_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] rw [if_neg hij] have hsum : (∑ k, R i k * s e k * R j k) = ∑ k, R i k * R j k * s e k := by apply Finset.sum_congr rfl intro k hk ring rw [hsum] ring have hlinear (e' e : E) : (s e' j - s e j) * R i j + (s e' i - s e i) * R j i = ((B * A e' * B.transpose) i j - (B * A e * B.transpose) i j) - ∑ k, R i k * R j k * (s e' k - s e k) := by rw [hformula e', hformula e] simp_rw [mul_sub] rw [Finset.sum_sub_distrib] ring let a := s e₁ j - s e₀ j let b := s e₁ i - s e₀ i let c := s e₂ j - s e₀ j let d := s e₂ i - s e₀ i let r₁ := ((B * A e₁ * B.transpose) i j - (B * A e₀ * B.transpose) i j) - ∑ k, R i k * R j k * (s e₁ k - s e₀ k) let r₂ := ((B * A e₂ * B.transpose) i j - (B * A e₀ * B.transpose) i j) - ∑ k, R i k * R j k * (s e₂ k - s e₀ k) have heq₁ : a * R i j + b * R j i = r₁ := by simpa [a, b, r₁] using hlinear e₁ e₀ have heq₂ : c * R i j + d * R j i = r₂ := by simpa [c, d, r₂] using hlinear e₂ e₀ have hcoeff : |a| ≤ 2 * M ∧ |b| ≤ 2 * M ∧ |c| ≤ 2 * M ∧ |d| ≤ 2 * M := by have hdiff (e' e : E) (k : Fin p) : |s e' k - s e k| ≤ 2 * M := by calc |s e' k - s e k| ≤ |s e' k| + |s e k| := abs_sub _ _ _ ≤ M + M := add_le_add (hscale _ _) (hscale _ _) _ = 2 * M := by ring exact ⟨hdiff e₁ e₀ j, hdiff e₁ e₀ i, hdiff e₂ e₀ j, hdiff e₂ e₀ i⟩ have hdet' : δ ≤ |a * d - c * b| := by have heqdet : a * d - c * b = -pairAffineDet s i j e₀ e₁ e₂ := by simp [a, b, c, d, pairAffineDet] ring rw [heqdet, abs_neg] exact hdet have houtput (e' e : E) : |(B * A e' * B.transpose) i j - (B * A e * B.transpose) i j| ≤ 2 * ε := by calc |_ - _| ≤ |(B * A e' * B.transpose) i j| + |(B * A e * B.transpose) i j| := abs_sub _ _ _ ≤ ε + ε := add_le_add (happrox e' i j hij) (happrox e i j hij) _ = 2 * ε := by ring have hr₁ : |r₁| ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by dsimp [r₁] calc |_ - _| ≤ |(B * A e₁ * B.transpose) i j - (B * A e₀ * B.transpose) i j| + |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| := abs_sub _ _ _ ≤ 2 * ε + 2 * M * entryL2 R ^ 2 := add_le_add (houtput e₁ e₀) (coordinateProductRemainder_le s R hM hscale e₁ e₀ i j) _ = 2 * M * entryL2 R ^ 2 + 2 * ε := by ring have hr₂ : |r₂| ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by dsimp [r₂] calc |_ - _| ≤ |(B * A e₂ * B.transpose) i j - (B * A e₀ * B.transpose) i j| + |∑ k, R i k * R j k * (s e₂ k - s e₀ k)| := abs_sub _ _ _ ≤ 2 * ε + 2 * M * entryL2 R ^ 2 := add_le_add (houtput e₂ e₀) (coordinateProductRemainder_le s R hM hscale e₂ e₀ i j) _ = 2 * M * entryL2 R ^ 2 + 2 * ε := by ring have hη : 0 ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by positivity change |R i j| ≤ _ ∧ |R j i| ≤ _ exact pair_cramer_control hM hδ hη hcoeff hdet' heq₁ heq₂ hr₁ hr₂

-- Proof route: `B = (I+R)B₀`; comparing diagonal entries gives -- `R i i = -∑_{k≠i} R i k B₀ k i`, then apply Cauchy--Schwarz. theorem diagonalBranch_control {p : ℕ} (B₀ B : SqMatrix p) {c : ℝ} (hunit : IsUnit B₀.det) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hc : 0 ≤ c) (hoff : ∀ i j, i ≠ j → |transitionError B₀ B i j| ≤ c) : ∀ i, |transitionError B₀ B i i| ^ 2 ≤ ‖B₀‖ ^ 2 * ∑ k ∈ (Finset.univ.erase i), |transitionError B₀ B i k| ^ 2 := by classical let R := transitionError B₀ B have hRB : R * B₀ = B - B₀ := by dsimp [R, transitionError, transition] rw [Matrix.sub_mul, Matrix.one_mul] simpa only [Matrix.mul_assoc] using congrArg (fun X : SqMatrix p => X - B₀) (Matrix.nonsing_inv_mul_cancel_right B₀ B hunit) intro i have hentry := congrArg (fun X : SqMatrix p => X i i) hRB simp only [Matrix.mul_apply, Matrix.sub_apply, hdiag i, hdiag₀ i, sub_self] at hentry have hsplit := Finset.sum_erase_add (Finset.univ : Finset (Fin p)) (fun k => R i k * B₀ k i) (Finset.mem_univ i) have heq : R i i = -∑ k ∈ Finset.univ.erase i, R i k * B₀ k i := by rw [← hsplit, hdiag₀ i, mul_one] at hentry linarith have hcolumn : ∑ k ∈ Finset.univ.erase i, |B₀ k i| ^ 2 ≤ ‖B₀‖ ^ 2 := by let e : EuclideanSpace ℝ (Fin p) := toLp 2 (single i 1) have he : ‖e‖ = 1 := by simp [e] have hmul := Matrix.l2_opNorm_mulVec B₀ e rw [he, mul_one] at hmul have hfull : ∑ k, |B₀ k i| ^ 2 ≤ ‖B₀‖ ^ 2 := by have hsquare := (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mpr hmul rw [EuclideanSpace.norm_sq_eq] at hsquare simpa [e, mulVec, dotProduct, sq_abs] using hsquare exact (Finset.sum_le_sum_of_subset_of_nonneg (Finset.erase_subset _ _) (fun _ _ _ => sq_nonneg _)).trans hfull change |R i i| ^ 2 ≤ ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 rw [heq, abs_neg, sq_abs] calc (∑ k ∈ Finset.univ.erase i, R i k * B₀ k i) ^ 2 ≤ (∑ k ∈ Finset.univ.erase i, (R i k) ^ 2) * ∑ k ∈ Finset.univ.erase i, (B₀ k i) ^ 2 := Finset.sum_mul_sq_le_sq_mul_sq _ _ _ _ = (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) * ∑ k ∈ Finset.univ.erase i, |B₀ k i| ^ 2 := by simp only [sq_abs] _ ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) * ‖B₀‖ ^ 2 := by exact mul_le_mul_of_nonneg_left hcolumn (sum_nonneg fun _ _ => sq_nonneg _) _ = ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by ring

theorem entryL2_transitionError_le {p : ℕ} (B₀ B : SqMatrix p) {L c : ℝ} (hp : 0 < p) (hL : 0 ≤ L) (hc : 0 ≤ c) (hunit : IsUnit B₀.det) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hoff : ∀ i j, i ≠ j → |transitionError B₀ B i j| ≤ c) : entryL2 (transitionError B₀ B) ≤ c * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) := by classical let R := transitionError B₀ B have hdiagControl := diagonalBranch_control B₀ B hunit hdiag₀ hdiag hc hoff have hnormsq : ‖B₀‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr hB₀ have hoffSq (i k : Fin p) (hik : i ≠ k) : |R i k| ^ 2 ≤ c ^ 2 := by exact (sq_le_sq₀ (abs_nonneg _) hc).mpr (by simpa [R] using hoff i k hik) have herase (i : Fin p) : ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 ≤ (p - 1 : ℕ) * c ^ 2 := by calc ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 ≤ (Finset.univ.erase i).card • c ^ 2 := Finset.sum_le_card_nsmul _ _ _ (fun k hk => hoffSq i k (by simpa [ne_comm] using (Finset.mem_erase.mp hk).1)) _ = (p - 1 : ℕ) * c ^ 2 := by rw [Finset.card_erase_of_mem (Finset.mem_univ i), Finset.card_univ, Fintype.card_fin] norm_num have hrow (i : Fin p) : ∑ k, |R i k| ^ 2 ≤ (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by have hsplit := Finset.sum_erase_add (Finset.univ : Finset (Fin p)) (fun k => |R i k| ^ 2) (Finset.mem_univ i) rw [← hsplit] calc (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + |R i i| ^ 2 ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr simpa [R] using hdiagControl i _ ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + L ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr _ = (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by ring have hsum : ∑ i, ∑ k, |R i k| ^ 2 ≤ (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := by calc ∑ i, ∑ k, |R i k| ^ 2 ≤ ∑ i, (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr with i exact hrow i _ ≤ ∑ _i : Fin p, (1 + L ^ 2) * ((p - 1 : ℕ) * c ^ 2) := by gcongr with i exact herase i _ = (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := by simp [Finset.card_univ, Fintype.card_fin] ring rw [entryL2_eq_sqrt, Real.sqrt_le_iff] constructor · positivity · calc ∑ i, ∑ j, |R i j| ^ 2 ≤ (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := hsum _ = (c * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2))) ^ 2 := by rw [mul_pow, Real.sq_sqrt] · ring · positivity

theorem opNorm_le_entryL2 {p : ℕ} (R : SqMatrix p) : ‖R‖ ≤ entryL2 R := by rw [Matrix.cstar_norm_def] calc ‖(Matrix.toEuclideanCLM (n := Fin p) (𝕜 := ℝ)) R‖ ≤ @norm (SqMatrix p) Matrix.frobeniusNormedAddCommGroup.toNorm R := l2CLM_norm_le_frobenius R _ = entryL2 R := rfl

theorem sub_eq_transitionError_mul {p : ℕ} (B₀ B : SqMatrix p) (hunit : IsUnit B₀.det) : B - B₀ = transitionError B₀ B * B₀ := by rw [transitionError, Matrix.sub_mul, Matrix.one_mul, transition] rw [Matrix.nonsing_inv_mul_cancel_right B₀ B hunit]

-- Proof route: `pairwise_offDiagonal_control` and `entryL2_transitionError_le` give -- `u ≤ K (2 M u² + 2ε)`. The second identity-branch inequality absorbs the quadratic -- term, yielding `u ≤ 4Kε`. Factor `B-B₀ = R B₀`, use -- `‖R‖op ≤ entryL2 R`, and weaken `4KL` to the displayed `16KL³` using `1 ≤ L`. theorem opNorm_sub_le_of_pairwise_affine_in_identity_branch {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ L ε : ℝ} (hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hε : 0 ≤ ε) (happrox : OffDiagonalApproximateCongruence A B ε) (hbranch : InIdentityBranch M δ L B₀ B) : ‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * ε := by let R := transitionError B₀ B let K := pairwiseAggregateFactor p M δ L have hL0 : 0 ≤ L := le_trans (by norm_num) hL have hK0 : 0 ≤ K := by dsimp [K, pairwiseAggregateFactor, pairwiseSolveFactor] positivity have hu0 : 0 ≤ entryL2 R := entryL2_nonneg R have hc0 : 0 ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) := by unfold pairwiseSolveFactor positivity have hoff : ∀ i j, i ≠ j → |R i j| ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) := by simpa [R] using pairwise_offDiagonal_control A s B₀ B hM.le hδ hε hscale hsep hunit hexact happrox have hu := entryL2_transitionError_le B₀ B hp hL0 hc0 hunit hdiag₀ hdiag hB₀ hoff have huK : entryL2 R ≤ K * (2 * M * entryL2 R ^ 2 + 2 * ε) := by change entryL2 R ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) at hu calc entryL2 R ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) := hu _ = K * (2 * M * entryL2 R ^ 2 + 2 * ε) := by dsimp [K, pairwiseAggregateFactor] ring have hbranch' : 2 * K * M * entryL2 R ≤ 1 / 2 := by simpa [R, K, InIdentityBranch] using hbranch.2 have hquad : K * (2 * M * entryL2 R ^ 2) ≤ entryL2 R / 2 := by nlinarith [mul_nonneg hu0 (sub_nonneg.mpr hbranch')] have huLinear : entryL2 R ≤ 4 * K * ε := by nlinarith rw [sub_eq_transitionError_mul B₀ B hunit] calc ‖transitionError B₀ B * B₀‖ ≤ ‖transitionError B₀ B‖ * ‖B₀‖ := norm_mul_le _ _ _ ≤ entryL2 R * L := by exact mul_le_mul (by simpa [R] using opNorm_le_entryL2 R) hB₀ (norm_nonneg _) hu0 _ ≤ (4 * K * ε) * L := by gcongr _ ≤ pairwiseStabilityConstant p M δ L * ε := by unfold pairwiseStabilityConstant dsimp [K] have hL3 : 1 ≤ L ^ 3 := one_le_pow₀ hL have hcoef : 4 * L ≤ 16 * L ^ 3 := by nlinarith calc (4 * pairwiseAggregateFactor p M δ L * ε) * L = (pairwiseAggregateFactor p M δ L * ε) * (4 * L) := by ring _ ≤ (pairwiseAggregateFactor p M δ L * ε) * (16 * L ^ 3) := mul_le_mul_of_nonneg_left hcoef (mul_nonneg hK0 hε) _ = 16 * pairwiseAggregateFactor p M δ L * L ^ 3 * ε := by ring

theorem opNorm_sub_le_of_pairwise_affine {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ L J ε : ℝ} (hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hJ : 0 < J) (hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hinv : ‖B₀⁻¹‖ ≤ J) (hε : 0 ≤ ε) (hsmall : ε ≤ pairwiseResidualRadius p M δ L) (happrox : OffDiagonalApproximateCongruence A B ε) (hlocal : InReferenceNeighborhood (pairwiseLocalRadius p M δ L J) B₀ B) : ‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * ε := by have hbranch := inIdentityBranch_of_small_residual A s B₀ B hp hM hδ hL hJ hscale hsep hunit hexact hdiag₀ hdiag hB₀ hinv hε hsmall happrox hlocal exact opNorm_sub_le_of_pairwise_affine_in_identity_branch A s B₀ B hp hM hδ hL hscale hsep hunit hexact hdiag₀ hdiag hB₀ hε happrox hbranch