Discovery.Linear­Disentanglement.Quantitative

theorem simultaneousCongruenceResidual_nonneg {d : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix d) (s : E → Fin d → ℝ) (B : SqMatrix d) : 0 ≤ simultaneousCongruenceResidual A s B := by classical let e : E := choice ‹Nonempty E› exact (norm_nonneg _).trans (Finset.le_sup' (fun e => ‖congruenceDefect (A e) (s e) B‖) (Finset.mem_univ e))

theorem productControlFactor_pos {d : ℕ} {L δ : ℝ} (hd : 0 < d) (hL : 0 < L) (hδ : 0 < δ) : 0 < productControlFactor d L δ := by unfold productControlFactor affineSolveFactor positivity

theorem admissibleRadius_pos {d : ℕ} {L δ R : ℝ} (hd : 0 < d) (hL : 0 < L) (hδ : 0 < δ) (hR : 0 < R) : 0 < admissibleRadius d L δ R := by have hq : 0 < productControlFactor d L δ := productControlFactor_pos hd hL hδ unfold admissibleRadius positivity

-- Proof route: matrix multiplication, transpose, subtraction, diagonal constants, and -- the norm are continuous in finite dimension; close under the finite nonempty `sup'`. theorem continuous_simultaneousCongruenceResidual {d : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix d) (s : E → Fin d → ℝ) : Continuous (simultaneousCongruenceResidual A s) := by classical unfold simultaneousCongruenceResidual have h : Continuous (Finset.univ.sup' univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖)) := by apply Continuous.finset_sup' univ_nonempty intro e _ apply Continuous.norm unfold congruenceDefect fun_prop rw [show (fun B => Finset.univ.sup' univ_nonempty (fun e => ‖congruenceDefect (A e) (s e) B‖)) = Finset.univ.sup' univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖) by funext B exact (Finset.sup'_apply univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖) B).symm] exact h

theorem sqMatrix_uniformCompactCorrespondence_dichotomy {P : Type*} [TopologicalSpace P] [T2Space P] {d : ℕ} (K : Set (P × SqMatrix d)) (B₀ : P → SqMatrix d) (r : P × SqMatrix d → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hB₀ : Continuous B₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p B, (p, B) ∈ K → r (p, B) = 0 → B = B₀ p) : farFeasibleSet K B₀ ρ = ∅ ∨ Nonempty (UniformPositiveExclusionRadius K B₀ ρ r) := by exact uniformCompactCorrespondence_dichotomy K B₀ r ρ hK hB₀ hr_cont hρ_cont hρ_pos hr_nonneg hr_zero

theorem exists_sqMatrix_uniformExclusionTolerance {P : Type*} [TopologicalSpace P] [T2Space P] {d : ℕ} (K : Set (P × SqMatrix d)) (B₀ : P → SqMatrix d) (r : P × SqMatrix d → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hB₀ : Continuous B₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p B, (p, B) ∈ K → r (p, B) = 0 → B = B₀ p) : ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ p B, (p, B) ∈ K → r (p, B) ≤ ε₀ → ‖B - B₀ p‖ < ρ p := by simpa only [dist_eq_norm] using (exists_uniformExclusionTolerance_le K B₀ r ρ hK hB₀ hr_cont hρ_cont hρ_pos hr_nonneg hr_zero)

theorem abs_entry_le_opNorm {d : ℕ} (M : SqMatrix d) (i j : Fin d) : |M i j| ≤ ‖M‖ := by classical let e : EuclideanSpace ℝ (Fin d) := toLp 2 (single j 1) have he : ‖e‖ = 1 := by simp [e] have hcoord : |((EuclideanSpace.equiv (Fin d) ℝ).symm (M *ᵥ e)) i| ≤ ‖(EuclideanSpace.equiv (Fin d) ℝ).symm (M *ᵥ e)‖ := by simpa only [Real.norm_eq_abs] using PiLp.norm_apply_le ((EuclideanSpace.equiv (Fin d) ℝ).symm (M *ᵥ e)) i calc |M i j| = |((EuclideanSpace.equiv (Fin d) ℝ).symm (M *ᵥ e)) i| := by simp [e] _ ≤ ‖(EuclideanSpace.equiv (Fin d) ℝ).symm (M *ᵥ e)‖ := hcoord _ ≤ ‖M‖ * ‖e‖ := Matrix.l2_opNorm_mulVec M e _ = ‖M‖ := by rw [he, mul_one]

theorem opNorm_le_dimension_mul_of_entry_bound {d : ℕ} (M : SqMatrix d) {c : ℝ} (hc : 0 ≤ c) (hM : ∀ i j, |M i j| ≤ c) : ‖M‖ ≤ (d : ℝ) * c := by rw [Matrix.cstar_norm_def] calc ‖(Matrix.toEuclideanCLM (n := Fin d) (𝕜 := ℝ)) M‖ ≤ @norm (SqMatrix d) Matrix.frobeniusNormedAddCommGroup.toNorm M := l2CLM_norm_le_frobenius M _ = sqrt (∑ i, ∑ j, |M i j| ^ 2) := by rw [Matrix.frobenius_norm_def, Real.sqrt_eq_rpow] simp only [Real.rpow_two, Real.norm_eq_abs] _ ≤ (d : ℝ) * c := by rw [Real.sqrt_le_iff] constructor · positivity · calc ∑ i, ∑ j, |M i j| ^ 2 ≤ ∑ _i : Fin d, ∑ _j : Fin d, c ^ 2 := by gcongr with i j exact hM i j _ = ((d : ℝ) * c) ^ 2 := by simp [Finset.sum_const, nsmul_eq_mul] ring

-- Proof route: use `V⁻¹ *ᵥ (V *ᵥ x) = x`, expand `V⁻¹` through the adjugate (or use -- `Matrix.det_smul_inv_mulVec_eq_cramer`), expand each `(d-1)`-minor determinant, and -- bound its `factorial (d-1)` Leibniz terms by `(2L)^(d-1)`. theorem coordinate_le_affineSolveFactor {d : ℕ} (V : SqMatrix d) (x : Fin d → ℝ) {L δ η : ℝ} (hδ : 0 < δ) (hL : 0 ≤ L) (hV : ∀ i j, |V i j| ≤ 2 * L) (hdet : δ ≤ |V.det|) (hres : ∀ i, |(V *ᵥ x) i| ≤ η) : ∀ j, |x j| ≤ affineSolveFactor d L δ * η := by classical intro j have hdet0 : V.det ≠ 0 := by intro h rw [h, abs_zero] at hdet linarith have hunit : IsUnit V.det := isUnit_iff_ne_zero.mpr hdet0 let b := V *ᵥ x have hx : V⁻¹ *ᵥ b = x := by rw [show b = V *ᵥ x from rfl, Matrix.mulVec_mulVec, Matrix.nonsing_inv_mul V hunit, Matrix.one_mulVec] have hcramer := congrFun (V.det_smul_inv_mulVec_eq_cramer b hunit) j have heq : V.det * x j = (V.updateCol j b).det := by simpa [hx, Matrix.cramer_apply] using hcramer have hbound : |(V.updateCol j b).det| ≤ (Nat.factorial d : ℝ) * (2 * L) ^ (d - 1) * η := abs_det_updateCol_le V b j (by positivity) hV hres have hmul : δ * |x j| ≤ (Nat.factorial d : ℝ) * (2 * L) ^ (d - 1) * η := by calc δ * |x j| ≤ |V.det| * |x j| := by gcongr _ = |(V.updateCol j b).det| := by rw [← abs_mul, heq] _ ≤ _ := hbound have hd0 : d ≠ 0 := Nat.ne_of_gt (Fin.pos_iff_nonempty.mpr ⟨j⟩) have hfac : (d : ℝ) * (Nat.factorial (d - 1) : ℝ) = (Nat.factorial d : ℝ) := by norm_cast exact Nat.mul_factorial_pred hd0 unfold affineSolveFactor rw [mul_assoc, div_mul_eq_mul_div] apply (le_div_iff₀ hδ).2 calc |x j| * δ = δ * |x j| := mul_comm _ _ _ ≤ (Nat.factorial d : ℝ) * (2 * L) ^ (d - 1) * η := hmul _ = (d : ℝ) * ((Nat.factorial (d - 1) : ℝ) * (2 * L) ^ (d - 1)) * η := by rw [← hfac] ring

theorem transition_diagonal_congruence {d : ℕ} {E : Type*} [Fintype E] (A : E → SqMatrix d) (s : E → Fin d → ℝ) (B₀ B : SqMatrix d) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (e : E) : transition B₀ B * diagonal (s e) * (transition B₀ B).transpose = B * A e * B.transpose := by rw [← hexact e] unfold transition rw [Matrix.transpose_mul, Matrix.transpose_nonsing_inv] have hut : IsUnit B₀.transpose.det := Matrix.isUnit_det_transpose B₀ hunit calc (B * B₀⁻¹) * (B₀ * A e * B₀.transpose) * ((B₀.transpose)⁻¹ * B.transpose) = B * (B₀⁻¹ * B₀) * A e * (B₀.transpose * (B₀.transpose)⁻¹) * B.transpose := by noncomm_ring _ = B * A e * B.transpose := by rw [Matrix.nonsing_inv_mul B₀ hunit, Matrix.mul_nonsing_inv B₀.transpose hut] simp

-- Proof route: choose `base,pick` from `hsep`, subtract each picked congruence equation -- from the base equation, and apply `coordinate_le_affineSolveFactor`. On diagonal -- matrix entries solve for `M i a ^ 2 - 1_{i=a}`; off the diagonal solve for -- `M i a * M j a`. `abs_entry_le_opNorm` and the triangle inequality give `2ε`. theorem transition_coordinate_product_control {d : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix d) (s : E → Fin d → ℝ) (B₀ B : SqMatrix d) {L δ ε : ℝ} (hL : 0 ≤ L) (hδ : 0 < δ) (hscale : ShiftScaleBound s L) (hsep : AffineMinorSeparated s δ) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (happrox : ApproximateCongruence A s B ε) : (∀ i a, |(transition B₀ B i a) ^ 2 - if i = a then 1 else 0| ≤ productControlFactor d L δ * ε) ∧ (∀ i j a, i ≠ j → |transition B₀ B i a * transition B₀ B j a| ≤ productControlFactor d L δ * ε) := by classical obtain ⟨base, pick, hdet⟩ := hsep let M := transition B₀ B let V : SqMatrix d := fun k a => s (pick k) a - s base a have hV : ∀ k a, |V k a| ≤ 2 * L := by intro k a dsimp [V] calc |s (pick k) a - s base a| ≤ |s (pick k) a| + |s base a| := abs_sub _ _ _ ≤ L + L := add_le_add (hscale _ _) (hscale _ _) _ = 2 * L := by ring have hdef : ∀ e i j, |congruenceDefect (A e) (s e) B i j| ≤ ε := by intro e i j calc |congruenceDefect (A e) (s e) B i j| ≤ ‖congruenceDefect (A e) (s e) B‖ := abs_entry_le_opNorm _ _ _ _ ≤ ε := (simultaneousCongruenceResidual_le_iff A s B ε).mp happrox e have hdefM : ∀ e i j, |(M * diagonal (s e) * M.transpose - diagonal (s e)) i j| ≤ ε := by intro e i j rw [transition_diagonal_congruence A s B₀ B hunit hexact e] exact hdef e i j constructor · intro i a let y : Fin d → ℝ := fun b => M i b ^ 2 - if i = b then 1 else 0 have hres : ∀ k, |(V *ᵥ y) k| ≤ 2 * ε := by intro k have hid : (V *ᵥ y) k = ((M * diagonal (s (pick k)) * M.transpose - diagonal (s (pick k))) i i) - ((M * diagonal (s base) * M.transpose - diagonal (s base)) i i) := diagonal_difference_mulVec M (s (pick k)) (s base) i k rw [hid] calc |_ - _| ≤ |(M * diagonal (s (pick k)) * M.transpose - diagonal (s (pick k))) i i| + |(M * diagonal (s base) * M.transpose - diagonal (s base)) i i| := abs_sub _ _ _ ≤ ε + ε := add_le_add (hdefM _ _ _) (hdefM _ _ _) _ = 2 * ε := by ring have hy := coordinate_le_affineSolveFactor V y hδ hL hV hdet hres a change |M i a ^ 2 - if i = a then 1 else 0| ≤ _ change |y a| ≤ _ at hy unfold productControlFactor nlinarith · intro i j a hij let y : Fin d → ℝ := fun b => M i b * M j b have hres : ∀ k, |(V *ᵥ y) k| ≤ 2 * ε := by intro k have hid : (V *ᵥ y) k = ((M * diagonal (s (pick k)) * M.transpose - diagonal (s (pick k))) i j) - ((M * diagonal (s base) * M.transpose - diagonal (s base)) i j) := offDiagonal_difference_mulVec M (s (pick k)) (s base) i j k hij rw [hid] calc |_ - _| ≤ |(M * diagonal (s (pick k)) * M.transpose - diagonal (s (pick k))) i j| + |(M * diagonal (s base) * M.transpose - diagonal (s base)) i j| := abs_sub _ _ _ ≤ ε + ε := add_le_add (hdefM _ _ _) (hdefM _ _ _) _ = 2 * ε := by ring have hy := coordinate_le_affineSolveFactor V y hδ hL hV hdet hres a change |M i a * M j a| ≤ _ change |y a| ≤ _ at hy unfold productControlFactor nlinarith

-- Proof route: square control first gives `|M i a| ≤ sqrt(qε)` for `a ≠ i`. From -- `B = M B₀` and both unit diagonals, bound `|M i i - 1|` by the off-diagonal terms -- times entries of `B₀`, hence by `d R sqrt(qε)`. The second threshold makes this ≤ 1/2. theorem transition_diagonal_ge_half {d : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix d) (s : E → Fin d → ℝ) (B₀ B : SqMatrix d) {L δ R ε : ℝ} (hd : 0 < d) (hL : 0 < L) (hδ : 0 < δ) (hR : 0 < R) (hscale : ShiftScaleBound s L) (hsep : AffineMinorSeparated s δ) (hnorm₀ : UnitDiagonal B₀) (hnorm : UnitDiagonal B) (hmatrixScale : PairMatrixScaleBound R B₀ B) (hB₀unit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (hsmall : ε ≤ admissibleRadius d L δ R) (happrox : ApproximateCongruence A s B ε) : ∀ i, (1 : ℝ) / 2 ≤ transition B₀ B i i := by classical let q := productControlFactor d L δ let K := R let M := transition B₀ B have hq : 0 < q := productControlFactor_pos hd hL hδ have hK : 0 < K := by simpa [K] using hR have hcontrol := transition_coordinate_product_control A s B₀ B hL.le hδ hscale hsep hB₀unit hexact happrox have heps : ε ≤ 1 / (4 * (d : ℝ) ^ 2 * K ^ 2 * q) := by exact hsmall.trans (min_le_right _ _) have hqeps : q * ε ≤ (1 / (2 * (d : ℝ) * K)) ^ 2 := by calc q * ε ≤ q * (1 / (4 * (d : ℝ) ^ 2 * K ^ 2 * q)) := mul_le_mul_of_nonneg_left heps hq.le _ = (1 / (2 * (d : ℝ) * K)) ^ 2 := by field_simp [ne_of_gt hq, ne_of_gt hK, Nat.cast_ne_zero.mpr (Nat.ne_of_gt hd)] ring have hoff : ∀ i a, i ≠ a → |M i a| ≤ 1 / (2 * (d : ℝ) * K) := by intro i a hia have hsquare := hcontrol.1 i a change |M i a ^ 2 - (if i = a then 1 else 0)| ≤ q * ε at hsquare simp only [if_neg hia, sub_zero, abs_sq] at hsquare apply (sq_le_sq₀ (abs_nonneg _) (by positivity)).mp rw [sq_abs] exact hsquare.trans hqeps have hB₀entry : ∀ a i, |B₀ a i| ≤ R := by intro a i exact (abs_entry_le_opNorm B₀ a i).trans hmatrixScale.1 have hMB : M * B₀ = B := by dsimp [M, transition] simpa only [Matrix.mul_assoc] using Matrix.nonsing_inv_mul_cancel_right B₀ B hB₀unit intro i have hentry := congrArg (fun N : SqMatrix d => N i i) hMB simp only [Matrix.mul_apply] at hentry have hsplit := Finset.sum_erase_add (Finset.univ : Finset (Fin d)) (fun a => M i a * B₀ a i) (Finset.mem_univ i) rw [← hsplit] at hentry rw [hnorm₀ i, mul_one, hnorm i] at hentry have heq : M i i - 1 = -∑ a ∈ Finset.univ.erase i, M i a * B₀ a i := by linarith have habs : |M i i - 1| ≤ 1 / 2 := by rw [heq, abs_neg] calc |∑ a ∈ Finset.univ.erase i, M i a * B₀ a i| ≤ ∑ a ∈ Finset.univ.erase i, |M i a * B₀ a i| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _a ∈ Finset.univ.erase i, 1 / (2 * (d : ℝ)) := by gcongr with a ha rw [abs_mul] have hia : i ≠ a := by exact fun h => (Finset.mem_erase.mp ha).1 h.symm calc |M i a| * |B₀ a i| ≤ (1 / (2 * (d : ℝ) * K)) * R := by gcongr · exact hoff i a hia · exact hB₀entry a i _ ≤ 1 / (2 * (d : ℝ)) := by have hRK : R ≤ K := by simp [K] field_simp [Nat.cast_ne_zero.mpr (Nat.ne_of_gt hd), ne_of_gt hK] nlinarith _ ≤ ∑ _a ∈ Finset.univ, 1 / (2 * (d : ℝ)) := by apply Finset.sum_le_sum_of_subset_of_nonneg (Finset.erase_subset _ _) intros positivity _ = 1 / 2 := by simp [Finset.sum_const, nsmul_eq_mul] field_simp [Nat.cast_ne_zero.mpr (Nat.ne_of_gt hd)] change (1 : ℝ) / 2 ≤ M i i have := (abs_le.mp habs).1 linarith