Discovery.LinearDisentanglement.Quantitative
Paper-independent finite-dimensional stability tools for approximate simultaneous congruence diagonalization: residuals, affine-minor separation, explicit operator-norm bounds, and compact exclusion radii.
Definitions 18 core · 3 supporting This module gives paper-independent definitions for the residual of a finite family of real congruence equations, quantitative affine separation of their prescribed diagonal vectors, normalization and conditioning assump ★ simultaneousCongruenceResidual_le_iff
Quantitative simultaneous-congruence stability: definitions
This module gives paper-independent definitions for the residual of a finite family of real congruence equations, quantitative affine separation of their prescribed diagonal vectors, normalization and conditioning assumptions, and the explicit constants used by the stability theorem.
The matrix norm in this API is the Euclidean (ℓ²) operator norm.
abbrev SqMatrix reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a nonnegative integer dimension, a square matrix is a real-valued matrix with that many rows and that many columns.
def congruenceDefect reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, an observed matrix, a prescribed diagonal vector, and a candidate change-of-coordinates matrix, the congruence defect is minus the diagonal matrix formed from the prescribed vector.
def simultaneousCongruenceResidual reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a nonempty finite environment collection, an observed matrix for each environment, a prescribed diagonal vector for each environment, and a candidate change-of-coordinates matrix, the simultaneous congruence residual is the largest Euclidean operator norm of the individual congruence defects across environments.
theorem simultaneousCongruenceResidual_le_iff reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a finite real matrix family, its prescribed diagonal shifts, a candidate change of coordinates, and a tolerance, the simultaneous residual is at most that tolerance exactly when every individual congruence defect is.
Formal statement
hypotheses
conclusion
simultaneousCongruenceResidual A s B ≤ ε ↔ ∀ e, ‖congruenceDefect (A e) (s e) B‖ ≤ ε
Proof (Lean source)
theorem simultaneousCongruenceResidual_le_iff {d : ℕ} {E : Type*}
[Fintype E] [Nonempty E] (A : E → SqMatrix d) (s : E → Fin d → ℝ)
(B : SqMatrix d) (ε : ℝ) :
simultaneousCongruenceResidual A s B ≤ ε ↔
∀ e, ‖congruenceDefect (A e) (s e) B‖ ≤ ε := by
classical
simp only [simultaneousCongruenceResidual, Finset.sup'_le_iff, Finset.mem_univ,
forall_const]
def AffineMinorSeparated reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a finite environment collection, a diagonal shift vector for each environment, and a real margin, affine minor separation holds when there exist one base environment and one selected environment for each coordinate such that the absolute determinant of their shift-difference matrix is at least the margin.
def ShiftScaleBound reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a finite environment collection, a diagonal shift vector for each environment, and a real bound, the shift-scale bound holds exactly when every coordinate of every prescribed diagonal shift has absolute value at most the bound.
def UnitDiagonal reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension and a square matrix, unit-diagonal normalization holds exactly when every diagonal entry of the matrix equals one.
Definition (Lean source)
def operatorConditionNumber reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension and a square matrix, its Euclidean operator-norm condition number is the product of its Euclidean operator norm and the Euclidean operator norm of its inverse. This is the condition number for a nonsingular matrix; for a singular matrix the inverse is zero by convention, so the value is zero, which is why every bound on it in this library is paired with a nonsingularity requirement.
Definition (Lean source)
def WellConditioned reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a real condition bound, and a square matrix, bounded conditioning holds exactly when the matrix is nonsingular and its Euclidean operator-norm condition number is at most the bound.
Definition (Lean source)
parameters
def
WellConditioned κ B :
Prop
def PairConditionBound reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a real condition bound, and a reference and candidate matrix, the pair condition bound holds exactly when the reference matrix is boundedly conditioned by that bound and the candidate matrix is boundedly conditioned by that bound.
Definition (Lean source)
parameters
def
PairConditionBound κ B₀ B :
Prop
def PairMatrixScaleBound reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a real scale bound, and a reference and candidate matrix, the pair matrix-scale bound holds exactly when the reference matrix's Euclidean operator norm is at most the scale bound and the candidate matrix's Euclidean operator norm is at most the scale bound.
Definition (Lean source)
parameters
def
PairMatrixScaleBound R B₀ B :
Prop
given by
clause 1
‖B₀‖ ≤ R
clause 2
‖B‖ ≤ R
def transition reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension and a reference and candidate matrix, the transition matrix is the candidate matrix multiplied by the inverse of the reference matrix.
def ExactCongruence reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a finite environment collection, an observed matrix for each environment, a prescribed diagonal vector for each environment, and a reference matrix, exact congruence holds exactly when, in every environment, the reference matrix transforms the observed matrix into the diagonal matrix prescribed there.
def ApproximateCongruence reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a nonempty finite environment collection, an observed matrix for each environment, a prescribed diagonal vector for each environment, a candidate matrix, and a real tolerance, approximate congruence holds exactly when the simultaneous congruence residual is at most the tolerance.
Definition (Lean source)
parameters
def
ApproximateCongruence A s B ε :
Prop
given by
simultaneousCongruenceResidual A s B ≤ ε
def affineSolveFactor reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a shift scale, and an affine-separation margin, the affine solve factor is .
Definition (Lean source)
parameters
d :
ℕ
L δ :
ℝ
def
affineSolveFactor d L δ :
ℝ
given by
(d : ℝ) * (factorial (d - 1) : ℝ) * (2 * L) ^ (d - 1) / δ
def productControlFactor reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a shift scale, and an affine-separation margin, the product-control factor is twice the affine solve factor.
Definition (Lean source)
def stabilityConstant reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a shift scale, an affine-separation margin, a matrix scale, and a condition-number envelope, the stability constant is times the product-control factor.
Definition (Lean source)
parameters
d :
ℕ
L δ R κ :
ℝ
def
stabilityConstant d L δ R κ :
ℝ
given by
2 * (d : ℝ) * R * max 1 κ * productControlFactor d L δ
def admissibleRadius reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a dimension, a shift scale, an affine-separation margin, a matrix scale, and a condition-number envelope, the admissible residual radius is the smaller of the two displayed reciprocal bounds determined by those quantities.
Definition (Lean source)
parameters
d :
ℕ
L δ R κ :
ℝ
def
admissibleRadius d L δ R κ :
ℝ
given by
min (1 / (4 * productControlFactor d L δ)) (1 / (4 * (d : ℝ) ^ 2 * (R * max 1 κ) ^ 2 * productControlFactor d L δ))
3 supporting declarations (lemmas, instances)
-
simultaneousCongruenceResidual_nonnegtheorem — For a finite real matrix family, its prescribed diagonal shifts, and a candidate change of coordinates, the simultaneous-congruence residual is nonnegative.hypothesesconclusion0 ≤ simultaneousCongruenceResidual A s BProof (Lean source)
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)) -
productControlFactor_postheorem — When the matrix dimension is positive, the shift scale is positive, and the affine separation margin is positive, the coordinate-product amplification factor is strictly positive.Proof (Lean source)
theorem productControlFactor_pos {d : ℕ} {L δ : ℝ} (hd : 0 < d) (hL : 0 < L) (hδ : 0 < δ) : 0 < productControlFactor d L δ := by unfold productControlFactor affineSolveFactor positivity -
admissibleRadius_postheorem — When the matrix dimension is positive, the shift scale is positive, the affine separation margin is positive, and the matrix scale is positive, the declared small-residual radius is strictly positive.hypothesesd :ℕL δ R κ :ℝhd :0 < dhL :0 < Lhδ :0 < δhR :0 < Rconclusion0 < admissibleRadius d L δ R κProof (Lean source)
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 have hmax : 0 < max 1 κ := lt_of_lt_of_le zero_lt_one (le_max_left _ _) positivity
CompactExclusion 1 core · 3 supporting This module specializes the generic compact-exclusion API of Causalean.Mathlib.Topology.CompactExclusion to real square matrices. ★ exists_simultaneousCongruence_exclusionRadius
Compact exclusion for simultaneous congruence
This module specializes the generic compact-exclusion API of
Causalean.Mathlib.Topology.CompactExclusion to real square matrices. It shows that the
simultaneous-congruence residual is continuous, so on a compact candidate set whose only
zero-residual candidate is a reference matrix, the residual has a strictly positive attained
minimum outside any open neighborhood of the reference. It also restates the uniform
compact-correspondence dichotomy and residual tolerance for parameter-matrix correspondences, with
distance measured by the Euclidean operator norm.
theorem exists_simultaneousCongruence_exclusionRadius reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
For a finite nonempty real matrix family, its diagonal shifts, a candidate set of matrices, an open local chart, and a reference matrix, if the candidate set is compact, the chart is open, the reference is a candidate, the reference lies in the chart, the far candidates are nonempty, and only the reference has zero residual among candidates, then the far candidates have a strictly positive attained simultaneous-congruence residual minimum.
Formal statement
hypotheses
d :
ℕ
E :
A :
E → SqMatrix d
s :
E → Fin d → ℝ
B₀ :
SqMatrix d
hK :
hU :
IsOpen U
hB₀K :
B₀ ∈ K
hB₀U :
B₀ ∈ U
hfar :
(K \ U).Nonempty
hzero :
∀ B ∈ K
if
simultaneousCongruenceResidual A s B = 0
then
B = B₀
conclusion
Nonempty (PositiveExclusionRadius K U (simultaneousCongruenceResidual A s))
Proof (Lean source)
theorem exists_simultaneousCongruence_exclusionRadius {d : ℕ} {E : Type*}
[Fintype E] [Nonempty E]
(A : E → SqMatrix d) (s : E → Fin d → ℝ)
(K U : Set (SqMatrix d)) (B₀ : SqMatrix d)
(hK : IsCompact K) (hU : IsOpen U) (hB₀K : B₀ ∈ K) (hB₀U : B₀ ∈ U)
(hfar : (K \ U).Nonempty)
(hzero : ∀ B ∈ K, simultaneousCongruenceResidual A s B = 0 → B = B₀) :
Nonempty (PositiveExclusionRadius K U (simultaneousCongruenceResidual A s)) := by
exact exists_positiveExclusionRadius K U
(simultaneousCongruenceResidual A s) B₀
hK hU hB₀K hB₀U hfar
(continuous_simultaneousCongruenceResidual A s)
(fun B _ => simultaneousCongruenceResidual_nonneg A s B)
hzero
3 supporting declarations (lemmas, instances)
-
continuous_simultaneousCongruenceResidualtheorem — For a finite real matrix family and its prescribed diagonal shifts, the simultaneous-congruence residual is continuous as a function of the candidate matrix.hypothesesconclusionProof (Lean source)
-- 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' Finset.univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖)) := by apply Continuous.finset_sup' Finset.univ_nonempty intro e _ apply Continuous.norm unfold congruenceDefect fun_prop rw [show (fun B => Finset.univ.sup' Finset.univ_nonempty (fun e => ‖congruenceDefect (A e) (s e) B‖)) = Finset.univ.sup' Finset.univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖) by funext B exact (Finset.sup'_apply Finset.univ_nonempty (fun e B => ‖congruenceDefect (A e) (s e) B‖) B).symm] exact h -
sqMatrix_uniformCompactCorrespondence_dichotomytheorem — Given a parameter-matrix correspondence, a reference matrix section, a residual, and a radius function, if the correspondence is compact, the reference matrix section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference matrix has zero residual among feasible pairs, then either no operator-norm-far pair exists or one attains a strictly positive uniform residual minimum.hypothesesP :d :ℕB₀ :P → SqMatrix dr :P × SqMatrix d → ℝρ :P → ℝhK :hB₀ :Continuous B₀hr_cont :hρ_cont :hρ_pos :∀ p, 0 < ρ phr_nonneg :∀ z ∈ K, 0 ≤ r zhr_zero :∀ p Bif(p, B) ∈ Kandr (p, B) = 0thenB = B₀ pconclusionfarFeasibleSet K B₀ ρ = ∅ ∨ Nonempty (UniformPositiveExclusionRadius K B₀ ρ r)Proof (Lean source)
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 -
exists_sqMatrix_uniformExclusionTolerancetheorem — Given a parameter-matrix correspondence, a reference matrix section, a residual, and a radius function, if the correspondence is compact, the reference matrix section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference matrix has zero residual among feasible pairs, then one positive residual tolerance puts every feasible pair at or below it strictly inside its parameter-dependent Euclidean operator-norm reference ball.hypothesesP :d :ℕB₀ :P → SqMatrix dr :P × SqMatrix d → ℝρ :P → ℝhK :hB₀ :Continuous B₀hr_cont :hρ_cont :hρ_pos :∀ p, 0 < ρ phr_nonneg :∀ z ∈ K, 0 ≤ r zhr_zero :∀ p Bif(p, B) ∈ Kandr (p, B) = 0thenB = B₀ pconclusion∃ ε₀ : ℝ,0 < ε₀conclusion 1p B :(p, B) ∈ Kr (p, B) ≤ ε₀‖B - B₀ p‖ < ρ pProof (Lean source)
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)
Quantitative 1 core · 6 supporting This module proves a finite-dimensional residual-to-distance estimate. ★ opNorm_sub_le_of_approximate_simultaneous_congruence
Explicit quantitative simultaneous-congruence stability
This module proves a finite-dimensional residual-to-distance estimate. Affine minor separation first controls coordinatewise products of the transition matrix. Unit-diagonal normalization and the explicit small-residual threshold select the reference branch, after which coordinate bounds convert to a Euclidean operator-norm bound.
theorem opNorm_sub_le_of_approximate_simultaneous_congruence reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.Quantitative
Explicit simultaneous-congruence stability. For positive matrix dimension, positive shift scale, positive affine separation, and positive matrix scale, if the diagonal shifts obey their scale bound, the shift family has a separated affine minor, the reference is unit-diagonal, the candidate is unit-diagonal, the pair obeys the matrix scale bound, the pair obeys the condition-number bound, the reference realizes every congruence exactly, the residual tolerance is nonnegative, the tolerance is admissibly small, and the candidate realizes the congruences up to that tolerance, then the candidate is within the explicit linear modulus times the tolerance of the reference in Euclidean operator norm.
Formal statement
hypotheses
d :
ℕ
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 :
hnorm₀ :
UnitDiagonal B₀
hnorm :
hmatrixScale :
PairMatrixScaleBound R B₀ B
hcond :
PairConditionBound κ B₀ B
hexact :
ExactCongruence A s B₀
hε :
0 ≤ ε
hsmall :
ε ≤ admissibleRadius d L δ R κ
happrox :
ApproximateCongruence A s B ε
conclusion
‖B - B₀‖ ≤ stabilityConstant d L δ R κ * ε
Proof (Lean source)
-- Proof route: the preceding half-bound and cross-product control give
-- `|M i a| ≤ 2qε` for `i ≠ a`; square control bounds `|M i i - 1|`. Convert this to
-- `‖M-I‖ ≤ 2d qε`, write `B-B₀ = (M-I)B₀`, use `‖B₀‖ ≤ R`, and weaken by
-- `1 ≤ max 1 κ`.
theorem opNorm_sub_le_of_approximate_simultaneous_congruence {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)
(hcond : PairConditionBound κ B₀ B)
(hexact : ExactCongruence A s B₀)
(hε : 0 ≤ ε) (hsmall : ε ≤ admissibleRadius d L δ R κ)
(happrox : ApproximateCongruence A s B ε) :
‖B - B₀‖ ≤ stabilityConstant d L δ R κ * ε := by
classical
let q := productControlFactor d L δ
let M := transition B₀ B
have hq : 0 < q := productControlFactor_pos hd hL hδ
have hqε : 0 ≤ q * ε := mul_nonneg hq.le hε
have hunit : IsUnit B₀.det := hcond.1.1
have hcontrol := transition_coordinate_product_control A s B₀ B hL.le hδ hscale hsep
hunit hexact happrox
have hhalf := transition_diagonal_ge_half A s B₀ B hd hL hδ hR hscale hsep
hnorm₀ hnorm hmatrixScale hcond hexact hε hsmall happrox
have hoff : ∀ i a, i ≠ a → |M i a| ≤ 2 * q * ε := by
intro i a hia
have hp := hcontrol.2 i a a hia
change |M i a * M a a| ≤ q * ε at hp
rw [abs_mul] at hp
have haa : (1 : ℝ) / 2 ≤ |M a a| :=
(show (1 : ℝ) / 2 ≤ M a a from hhalf a).trans (le_abs_self _)
have hmul : |M i a| * ((1 : ℝ) / 2) ≤ |M i a| * |M a a| :=
mul_le_mul_of_nonneg_left haa (abs_nonneg _)
nlinarith
have hdiag : ∀ i, |M i i - 1| ≤ 2 * q * ε := by
intro i
have hsquare := hcontrol.1 i i
simp only [if_pos rfl] at hsquare
change |M i i ^ 2 - 1| ≤ q * ε at hsquare
have hi : (1 : ℝ) / 2 ≤ M i i := hhalf i
have hplus : 1 ≤ |M i i + 1| := by
rw [abs_of_nonneg]
· linarith
· linarith
have hfactor : |M i i - 1| * |M i i + 1| = |M i i ^ 2 - 1| := by
rw [← abs_mul]
congr 1
ring
calc
|M i i - 1| ≤ |M i i - 1| * |M i i + 1| := by
nlinarith [mul_le_mul_of_nonneg_left hplus (abs_nonneg (M i i - 1))]
_ = |M i i ^ 2 - 1| := hfactor
_ ≤ q * ε := hsquare
_ ≤ 2 * q * ε := by nlinarith
have hentry : ∀ i a, |(M - 1) i a| ≤ 2 * q * ε := by
intro i a
by_cases hia : i = a
· subst a
simpa using hdiag i
· simpa [Matrix.sub_apply, Matrix.one_apply, hia] using hoff i a hia
have hMnorm : ‖M - 1‖ ≤ (d : ℝ) * (2 * q * ε) :=
opNorm_le_dimension_mul_of_entry_bound (M - 1) (by positivity) hentry
have hMB : M * B₀ = B := by
dsimp [M, transition]
simpa only [Matrix.mul_assoc] using
Matrix.nonsing_inv_mul_cancel_right B₀ B hunit
have hfactor : B - B₀ = (M - 1) * B₀ := by
rw [Matrix.sub_mul, Matrix.one_mul, hMB]
rw [hfactor]
calc
‖(M - 1) * B₀‖ ≤ ‖M - 1‖ * ‖B₀‖ := norm_mul_le _ _
_ ≤ ((d : ℝ) * (2 * q * ε)) * R := by
exact mul_le_mul hMnorm hmatrixScale.1 (norm_nonneg _) (by positivity)
_ = 2 * (d : ℝ) * R * q * ε := by ring
_ ≤ 2 * (d : ℝ) * R * max 1 κ * q * ε := by
have hm := mul_le_mul_of_nonneg_left (le_max_left (1 : ℝ) κ)
(show 0 ≤ 2 * (d : ℝ) * R * q * ε by positivity)
calc
2 * (d : ℝ) * R * q * ε = (2 * (d : ℝ) * R * q * ε) * 1 := by ring
_ ≤ (2 * (d : ℝ) * R * q * ε) * max 1 κ := hm
_ = 2 * (d : ℝ) * R * max 1 κ * q * ε := by ring
_ = stabilityConstant d L δ R κ * ε := by
dsimp [q]
unfold stabilityConstant
ring
6 supporting declarations (lemmas, instances)
-
abs_entry_le_opNormtheorem — For a real square matrix and a selected row and column, the absolute value of that entry is bounded by the Euclidean operator norm.Proof (Lean source)
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] -
opNorm_le_dimension_mul_of_entry_boundtheorem — For a real square matrix, if the proposed entry bound is nonnegative and every entry obeys that bound, its Euclidean operator norm is at most the dimension times the bound.hypothesesconclusion‖M‖ ≤ (d : ℝ) * cProof (Lean source)
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 -
coordinate_le_affineSolveFactortheorem — For a real square coefficient matrix and a solution vector, if the determinant margin is positive, the scale bound is nonnegative, every coefficient is bounded, the determinant has the stated margin, and the linear-system residual is uniformly bounded, every solution coordinate is bounded by the explicit Cramer's-rule factor times the residual bound.hypothesesd :ℕV :SqMatrix dx :Fin d → ℝL δ η :ℝhδ :0 < δhL :0 ≤ LhV :∀ i j, |V i j| ≤ 2 * Lhdet :δ ≤ |V.det|hres :∀ i, |(V *ᵥ x) i| ≤ ηj :conclusion|x j| ≤ affineSolveFactor d L δ * ηProof (Lean source)
-- 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 -
transition_diagonal_congruencetheorem — For a real matrix family, its diagonal shifts, an exact reference matrix, a candidate matrix, if the reference is invertible and it exactly realizes every prescribed congruence, then the transition matrix conjugates each reference diagonal into the candidate congruence.hypothesesd :ℕE :Type*Fintype EA :E → SqMatrix ds :E → Fin d → ℝB₀ B :SqMatrix dhunit :IsUnit B₀.dethexact :ExactCongruence A s B₀e :Econclusion= B * A e * B.transposeProof (Lean source)
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 -
transition_coordinate_product_controltheorem — For a finite real matrix family, its prescribed diagonal shifts, an exact reference, and a candidate, if the shift scale is nonnegative, the affine separation margin is positive, the shifts obey their scale bound, a separated affine minor exists, the reference is invertible, the reference realizes the congruences exactly, and the candidate has the stated approximate residual, then squared transition entries and cross-row products have the explicit coordinatewise residual bounds.hypothesesd :ℕE :A :E → SqMatrix ds :E → Fin d → ℝB₀ B :SqMatrix dL δ ε :ℝhL :0 ≤ Lhδ :0 < δhscale :ShiftScaleBound s Lhsep :hunit :IsUnit B₀.dethexact :ExactCongruence A s B₀happrox :ApproximateCongruence A s B εconclusionconclusion 1i a :|(transition B₀ B i a) ^ 2 - if i = a then 1 else 0| ≤ productControlFactor d L δ * εconclusion 2i j a :i ≠ jProof (Lean source)
-- 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 -
transition_diagonal_ge_halftheorem — For positive matrix dimension, positive shift scale, positive affine separation, and positive matrix scale, if the shifts have the declared scale, their affine minor is separated, the reference is unit-diagonal, the candidate is unit-diagonal, both matrices obey the scale bound, both matrices obey the condition bound, the reference congruences are exact, the residual tolerance is nonnegative, it is below the admissible radius, and the candidate is approximately congruent, then every transition diagonal entry is at least one half.hypothesesd :ℕE :A :E → SqMatrix ds :E → Fin d → ℝB₀ B :SqMatrix dL δ R κ ε :ℝhd :0 < dhL :0 < Lhδ :0 < δhR :0 < Rhscale :ShiftScaleBound s Lhsep :hnorm₀ :UnitDiagonal B₀hnorm :hmatrixScale :PairMatrixScaleBound R B₀ Bhcond :PairConditionBound κ B₀ Bhexact :ExactCongruence A s B₀hε :0 ≤ εhsmall :ε ≤ admissibleRadius d L δ R κhapprox :ApproximateCongruence A s B εi :conclusion(1 : ℝ) / 2 ≤ transition B₀ B i iProof (Lean source)
-- 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) (hcond : PairConditionBound κ B₀ B) (hexact : ExactCongruence A s B₀) (hε : 0 ≤ ε) (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 * max 1 κ let M := transition B₀ B have hq : 0 < q := productControlFactor_pos hd hL hδ have hmax : 0 < max 1 κ := lt_of_lt_of_le zero_lt_one (le_max_left _ _) have hK : 0 < K := mul_pos hR hmax have hunit : IsUnit B₀.det := hcond.1.1 have hcontrol := transition_coordinate_product_control A s B₀ B hL.le hδ hscale hsep hunit 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 hunit 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 dsimp [K] nlinarith [le_max_left (1 : ℝ) κ] 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