Mathlib.Analysis.SymmetricTensorPencil
Finite-dimensional symmetric-tensor-pencil recovery: contraction and conditioning bounds, generalized-eigenvalue perturbation, spectral matching, and a quantitative permutation-aligned local inverse.
Basic 16 core · 5 supporting This module fixes paper-independent array models for finite real tensors and factor matrices. ★ contractLast_frobeniusNorm_le
Finite tensors, contractions, and quantitative norms
This module fixes paper-independent array models for finite real tensors and factor matrices. It defines rank-one tensor powers, degree lifts, Frobenius norms, contraction against a family of probes, and the exact contracted factorization used by tensor-pencil arguments.
abbrev Vec reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
A finite real vector with p coordinates. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
abbrev FactorMatrix reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
A real matrix whose n columns are vectors with p coordinates. With its explicit inputs, the defined object is given by the displayed formula.
abbrev Tensor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
An order-r real tensor on a p-dimensional coordinate space, represented as an array. With its explicit inputs, the defined object is given by the displayed formula.
abbrev LiftIndex reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The ordered multi-index space used for a degree-d tensor-power lift. With its explicit inputs, the defined object is given by the displayed formula.
def finiteFrobeniusNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The Euclidean/Frobenius norm of a finite real array. With its explicit inputs, the defined object is given by the displayed formula.
def matrixFrobeniusNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The Frobenius norm of a finite real matrix. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def squareOperatorNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The Euclidean operator norm of a finite real square matrix. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
ι :
A :
Matrix ι ι ℝ
def
squareOperatorNorm A :
ℝ
given by
‖(Matrix.toEuclideanCLM (n := ι) (𝕜 := ℝ)) A‖
def leastColumnSingularValue reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The last domain-indexed singular value of a finite real matrix, i.e. the singular value at index one less than the number of columns. For a matrix with no columns the index is zero by natural subtraction; the results using it assume a nonempty column index. With its explicit inputs, the defined object is given by the displayed formula.
def dot reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The Euclidean dot product of two finite real vectors. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def rankOneTensor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The order-r rank-one tensor power of a vector. With its explicit inputs, the defined object is given by the displayed formula.
def decompositionTensor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The symmetric tensor represented by weighted rank-one tensor powers of the columns. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def liftedDirections reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The matrix whose columns are the ordered degree-d tensor powers of the factor columns. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
given by
fun I j => ∏ k, C (I k) j
def blockIndex reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Concatenate two degree-d indices and one degree-q index into an order-d+d+q index. With its explicit inputs, the defined object is given by the displayed formula.
def contractLast reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Contract the final q modes of an order-d+d+q tensor against a family of q probes. With its explicit inputs, the defined object is given by the displayed formula.
def pencilProbes reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The probe family containing q-1 copies of u followed by one copy of w, for positive q; for q = 0 it is the empty family. With its explicit inputs, the defined object is given by the displayed formula.
theorem contractLast_frobeniusNorm_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Contracting a finite tensor against probes of norm at most one cannot increase its Frobenius norm. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
conclusion
Proof (Lean source)
-- Proof route: identify each contraction as an inner product in the product probe index,
-- apply finite Cauchy--Schwarz, and sum the squared bounds over the two free index blocks.
theorem contractLast_frobeniusNorm_le {p d q : ℕ} (T : Tensor p (d + d + q))
(probes : Fin q → Vec p)
(hprobes : ∀ a, finiteFrobeniusNorm (probes a) ≤ 1) :
matrixFrobeniusNorm (contractLast T probes) ≤ finiteFrobeniusNorm T := by
have hsingle (a : Fin q) : ∑ i, probes a i ^ 2 ≤ 1 := by
have hsq := (sq_le_sq₀ (Real.sqrt_nonneg _) (by norm_num)).2 (hprobes a)
simpa [finiteFrobeniusNorm,
Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] using hsq
have henergy :
∑ K : Fin q → Fin p, (∏ a, probes a (K a)) ^ 2 ≤ 1 := by
calc
_ = ∏ a, ∑ i, probes a i ^ 2 := by
calc
_ = ∑ K : Fin q → Fin p, ∏ a, probes a (K a) ^ 2 := by
apply Finset.sum_congr rfl
intro K _
rw [Finset.prod_pow]
_ = _ := (Fintype.prod_sum
(fun a : Fin q => fun i : Fin p => probes a i ^ 2)).symm
_ ≤ 1 := Finset.prod_le_one
(fun a _ => sum_nonneg fun _ _ => sq_nonneg _)
(fun a _ => hsingle a)
have hpoint (I J : LiftIndex p d) :
(contractLast T probes I J) ^ 2 ≤
∑ K : Fin q → Fin p, T (blockIndex I J K) ^ 2 := by
have hcs := Finset.sum_mul_sq_le_sq_mul_sq (Finset.univ : Finset (Fin q → Fin p))
(fun K => T (blockIndex I J K)) (fun K => ∏ a, probes a (K a))
have hrow : 0 ≤ ∑ K : Fin q → Fin p, T (blockIndex I J K) ^ 2 :=
sum_nonneg fun _ _ => sq_nonneg _
calc
_ ≤ (∑ K : Fin q → Fin p, T (blockIndex I J K) ^ 2) *
(∑ K : Fin q → Fin p, (∏ a, probes a (K a)) ^ 2) := by
simpa [contractLast] using hcs
_ ≤ (∑ K : Fin q → Fin p, T (blockIndex I J K) ^ 2) * 1 :=
mul_le_mul_of_nonneg_left henergy hrow
_ = _ := mul_one _
rw [matrixFrobeniusNorm, finiteFrobeniusNorm, finiteFrobeniusNorm]
apply Real.sqrt_le_sqrt
change (∑ x : LiftIndex p d × LiftIndex p d,
(contractLast T probes x.1 x.2) ^ 2) ≤ ∑ L, T L ^ 2
rw [Fintype.sum_prod_type]
calc
_ ≤ ∑ I, ∑ J, ∑ K : Fin q → Fin p, T (blockIndex I J K) ^ 2 := by
exact Finset.sum_le_sum fun I _ => Finset.sum_le_sum fun J _ => hpoint I J
_ = ∑ x : (LiftIndex p d × LiftIndex p d) × (Fin q → Fin p),
T (blockIndex x.1.1 x.1.2 x.2) ^ 2 := by
rw [Fintype.sum_prod_type, Fintype.sum_prod_type]
_ = _ := (blockIndexEquiv p d q).sum_comp (fun L => T L ^ 2)
5 supporting declarations (lemmas, instances)
-
squareOperatorNorm_le_matrixFrobeniustheorem — The Euclidean operator norm of a finite real square matrix is at most its entrywise Frobenius norm. The stated conclusion follows.Proof (Lean source)
theorem squareOperatorNorm_le_matrixFrobenius {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) : squareOperatorNorm A ≤ matrixFrobeniusNorm A := by rw [squareOperatorNorm] calc _ ≤ @norm (Matrix ι ι ℝ) Matrix.frobeniusNormedAddCommGroup.toNorm A := by open scoped Matrix.Norms.Frobenius in refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg A) fun x => ?_ have hmul := Matrix.frobenius_norm_mul A (Matrix.replicateCol Unit (ofLp x)) have heq : A * Matrix.replicateCol Unit (ofLp x) = Matrix.replicateCol Unit (mulVec A (ofLp x)) := by ext i u simp [Matrix.mul_apply, mulVec, Matrix.replicateCol, dotProduct] rw [heq, Matrix.frobenius_norm_replicateCol] at hmul rw [← Matrix.toEuclideanCLM_toLp A (ofLp x), WithLp.toLp_ofLp] at hmul simpa using hmul _ = matrixFrobeniusNorm A := by rw [Matrix.frobenius_norm_def, matrixFrobeniusNorm, finiteFrobeniusNorm, Real.sqrt_eq_rpow, Fintype.sum_prod_type] simp only [Real.rpow_two, Real.norm_eq_abs, sq_abs] -
contractLast_operatorNorm_letheorem — The operator norm of a contracted tensor is bounded by the original tensor's Frobenius norm when every contraction probe has norm at most one. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionProof (Lean source)
-- Proof route: first bound the square-matrix operator norm by its Frobenius norm, then invoke -- `contractLast_frobeniusNorm_le`. theorem contractLast_operatorNorm_le {p d q : ℕ} (T : Tensor p (d + d + q)) (probes : Fin q → Vec p) (hprobes : ∀ a, finiteFrobeniusNorm (probes a) ≤ 1) : squareOperatorNorm (contractLast T probes) ≤ finiteFrobeniusNorm T := by exact (squareOperatorNorm_le_matrixFrobenius (contractLast T probes)).trans (contractLast_frobeniusNorm_le T probes hprobes) -
contractLast_decompositionTensortheorem — Contracting a weighted symmetric rank-one decomposition against q-1 copies of u and one copy of w gives the lifted factor matrix times the corresponding diagonal loadings times its transpose. Under the listed assumptions, the stated conclusion follows.hypothesesconclusion= liftedDirections d C * diagonal (fun j => lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j)) * (liftedDirections d C).transposeProof (Lean source)
-- Proof route: ext the two free multi-indices, unfold both matrix products and the tensor sum, -- swap finite sums, and factor each probe sum into a dot product. theorem contractLast_decompositionTensor {p n d q : ℕ} (hq : 0 < q) (C : FactorMatrix p n) (lam : Fin n → ℝ) (u w : Vec p) : contractLast (decompositionTensor (d + d + q) C lam) (pencilProbes u w) = liftedDirections d C * diagonal (fun j => lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j)) * (liftedDirections d C).transpose := by classical ext I J rw [Matrix.mul_apply] simp_rw [Matrix.mul_diagonal, Matrix.transpose_apply] rw [contractLast] simp_rw [decompositionTensor, Finset.sum_mul] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro j _ have hrank (K : Fin q → Fin p) : rankOneTensor (d + d + q) (C.col j) (blockIndex I J K) = liftedDirections d C I j * liftedDirections d C J j * ∏ a, C (K a) j := by rw [rankOneTensor, Fin.prod_univ_add, Fin.prod_univ_add] simp only [Matrix.col_apply] congr 1 · congr 1 · apply Finset.prod_congr rfl intro i _ simp [blockIndex] · apply Finset.prod_congr rfl intro i _ simp only [blockIndex, Fin.addCases_left] rw [Fin.addCases_right] · apply Finset.prod_congr rfl intro i _ simp [blockIndex] simp_rw [hrank] have hprobe : (∑ K : Fin q → Fin p, (∏ a, C (K a) j) * ∏ a, pencilProbes u w a (K a)) = dot u (C.col j) ^ (q - 1) * dot w (C.col j) := by calc _ = ∑ K : Fin q → Fin p, ∏ a, (C (K a) j * pencilProbes u w a (K a)) := by apply Finset.sum_congr rfl intro K _ rw [Finset.prod_mul_distrib] _ = ∏ a, ∑ i, C i j * pencilProbes u w a i := (Fintype.prod_sum (fun a : Fin q => fun i : Fin p => C i j * pencilProbes u w a i)).symm _ = _ := by obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hq) rw [Fin.prod_univ_castSucc] simp only [pencilProbes] have hcast (a : Fin r) : ¬(a.castSucc.1 + 1 = r + 1) := by change ¬(a.1 + 1 = r + 1) have ha := a.isLt omega simp_rw [hcast, if_false] simp only [Fin.val_last, if_true] simp [dot, Finset.prod_const, mul_comm] calc _ = (lam j * liftedDirections d C I j * liftedDirections d C J j) * (∑ K : Fin q → Fin p, (∏ a, C (K a) j) * ∏ a, pencilProbes u w a (K a)) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro K _ ring _ = _ := by rw [hprobe]; ring -
finiteFrobeniusNorm_liftedColumn_eq_onetheorem — Unit columns have unit degree-d tensor lifts for every positive lifting degree. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionProof (Lean source)
-- Proof route: square the norm, factor the sum over functions `Fin d → Fin p` as a product of -- coordinate sums, and use the unit-column hypothesis in every factor. theorem finiteFrobeniusNorm_liftedColumn_eq_one {p n d : ℕ} (hd : 0 < d) (C : FactorMatrix p n) (hunit : ∀ j, finiteFrobeniusNorm (C.col j) = 1) (j : Fin n) : finiteFrobeniusNorm ((liftedDirections d C).col j) = 1 := by have hs : (∑ i, C i j ^ 2) = 1 := by have h := congrArg (fun z : ℝ => z ^ 2) (hunit j) simpa [finiteFrobeniusNorm, Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] using h rw [finiteFrobeniusNorm] have hp := show (∑ I : Fin d → Fin p, (∏ k, C (I k) j) ^ 2) = (∑ i, C i j ^ 2) ^ d by calc _ = ∑ I : Fin d → Fin p, ∏ k, C (I k) j ^ 2 := by apply Finset.sum_congr rfl intro I _ rw [Finset.prod_pow] _ = ∏ _k : Fin d, ∑ i, C i j ^ 2 := (Fintype.prod_sum (fun _k : Fin d => fun i : Fin p => C i j ^ 2)).symm _ = _ := by simp change sqrt (∑ I : Fin d → Fin p, (∏ k, C (I k) j) ^ 2) = 1 rw [hp, hs] simp -
matrixFrobeniusNorm_liftedDirectionstheorem — The Frobenius norm of a lifted factor matrix with unit original columns is the square root of the number of columns. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionProof (Lean source)
-- Proof route: regroup the matrix sum by columns and use -- `finiteFrobeniusNorm_liftedColumn_eq_one`. theorem matrixFrobeniusNorm_liftedDirections {p n d : ℕ} (hd : 0 < d) (C : FactorMatrix p n) (hunit : ∀ j, finiteFrobeniusNorm (C.col j) = 1) : matrixFrobeniusNorm (liftedDirections d C) = sqrt n := by have hcol (j : Fin n) : ∑ I : LiftIndex p d, (liftedDirections d C I j) ^ 2 = 1 := by have h := congrArg (fun z : ℝ => z ^ 2) (finiteFrobeniusNorm_liftedColumn_eq_one hd C hunit j) simpa [finiteFrobeniusNorm, Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] using h rw [matrixFrobeniusNorm, finiteFrobeniusNorm] congr 1 rw [Fintype.sum_prod_type, Finset.sum_comm] simp_rw [hcol] simp
SpectralMatching 4 core · 2 supporting This module isolates the two ingredients that precede spectral-projector perturbation: a finite-dimensional Bauer--Fike localization theorem for explicitly diagonalized real matrices, and the finite matching argument tha ★ exists_permutation_matching_of_localization
Spectral localization and finite matching
This module isolates the two ingredients that precede spectral-projector perturbation: a
finite-dimensional Bauer--Fike localization theorem for explicitly diagonalized real matrices,
and the finite matching argument that turns one-sided localization into a permutation under a
separation margin. It also records the elementary condition-number bound for coordinate
projectors. The localization convention is the spectral-norm Bauer--Fike bound used in the
robust simultaneous-diagonalization analysis of Goyal--Vempala--Xiao, arXiv:1306.5825,
perturbation.tex, Theorem thm:bauer.
def PairwiseGap reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
A real scalar family, over an arbitrary index type, has pairwise gap at least gap. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
ι :
Type*
values :
ι → ℝ
gap :
ℝ
i j :
i ≠ j
def
PairwiseGap values gap :
Prop
given by
gap ≤ |values i - values j|
def diagonalizableMatrix reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The conjugation of the diagonal matrix of the prescribed real entries by S, that is S times the diagonal times the inverse of S. It is diagonalized by S with those entries when S is invertible; for singular S the inverse is zero by convention and the value is the zero matrix. With its explicit inputs, the defined object is given by the displayed formula.
def coordinateProjector reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The coordinate projector selected by coordinate j of a diagonalizer S: S times the j-th standard diagonal unit matrix times the inverse of S. It is the rank-one spectral projector when S is invertible; for singular S the inverse is zero by convention and the value is the zero matrix. With its explicit inputs, the defined object is given by the displayed formula.
theorem exists_permutation_matching_of_localization reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
One-sided localization between two equally sized finite scalar families becomes a permutation matching when the source family is separated by more than twice the localization radius. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
n :
ℕ
values values' :
Fin n → ℝ
gap radius :
ℝ
hradius :
0 ≤ radius
hgap' :
PairwiseGap values' gap
hlocal :
∀ j', ∃ j, |values' j' - values j| ≤ radius
hsmall :
2 * radius < gap
Proof (Lean source)
-- Proof route: choose for every primed index one nearby unprimed index. Two primed indices
-- with the same choice would violate separation by the triangle inequality, so the choice map
-- is injective, hence bijective on the finite type; its inverse is the required permutation.
theorem exists_permutation_matching_of_localization {n : ℕ}
(values values' : Fin n → ℝ) {gap radius : ℝ}
(hradius : 0 ≤ radius) (hgap' : PairwiseGap values' gap)
(hlocal : ∀ j', ∃ j, |values' j' - values j| ≤ radius)
(hsmall : 2 * radius < gap) :
∃ pi : Perm (Fin n), ∀ j, |values' (pi j) - values j| ≤ radius := by
classical
choose f hf using hlocal
have hinj : Injective f := by
intro a b hab
by_contra hne
have hgapab : gap ≤ |values' a - values' b| := hgap' a b hne
have hdist : |values' a - values' b| ≤ 2 * radius := by
calc
|values' a - values' b|
= |(values' a - values (f a)) + (values (f b) - values' b)| := by
rw [hab]
congr 1
ring
_ ≤ |values' a - values (f a)| + |values (f b) - values' b| :=
abs_add_le _ _
_ = |values' a - values (f a)| + |values' b - values (f b)| := by
rw [abs_sub_comm (values (f b)) (values' b)]
_ ≤ radius + radius := add_le_add (hf a) (hf b)
_ = 2 * radius := by ring
exact (not_lt_of_ge (hgapab.trans hdist)) hsmall
have hbij : Bijective f := hinj.bijective_of_finite
let e : Perm (Fin n) := Equiv.ofBijective f hbij
refine ⟨e.symm, ?_⟩
intro j
change |values' ((Equiv.ofBijective f hbij).symm j) - values j| ≤ radius
have hfj : f ((Equiv.ofBijective f hbij).symm j) = j :=
Equiv.ofBijective_apply_symm_apply f hbij j
simpa [hfj] using hf ((Equiv.ofBijective f hbij).symm j)
2 supporting declarations (lemmas, instances)
-
coordinateProjector_operatorNorm_letheorem — Every coordinate projector of a diagonalizer has Euclidean operator norm at most the declared condition-number envelope. Under the listed assumptions, the stated conclusion follows.hypothesesn :ℕj :Fin nchi :ℝhS :IsUnit S.dethcondition :squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chiconclusionsquareOperatorNorm (coordinateProjector S j) ≤ chiProof (Lean source)
-- Proof route: use submultiplicativity twice, the fact that the one-coordinate diagonal -- projector has operator norm one, and the supplied bound on `‖S‖₂ ‖S⁻¹‖₂`. theorem coordinateProjector_operatorNorm_le {n : ℕ} (S : Matrix (Fin n) (Fin n) ℝ) (j : Fin n) {chi : ℝ} (hS : IsUnit S.det) (hcondition : squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi) : squareOperatorNorm (coordinateProjector S j) ≤ chi := by let _ : Nonempty (Fin n) := ⟨j⟩ unfold coordinateProjector squareOperatorNorm rw [Matrix.l2_opNorm_toEuclideanCLM] calc ‖S * diagonal (fun k => if k = j then (1 : ℝ) else 0) * S⁻¹‖ ≤ ‖S * diagonal (fun k => if k = j then (1 : ℝ) else 0)‖ * ‖S⁻¹‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖S‖ * ‖Matrix.diagonal (fun k => if k = j then (1 : ℝ) else 0)‖) * ‖S⁻¹‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ = ‖S‖ * ‖S⁻¹‖ := by rw [Matrix.l2_opNorm_diagonal] have hnorm : ‖(fun k : Fin n => if k = j then (1 : ℝ) else 0)‖ = 1 := by apply le_antisymm · apply (pi_norm_le_iff_of_nonempty _).2 intro k split <;> norm_num · simpa using norm_le_pi_norm (fun k : Fin n => if k = j then (1 : ℝ) else 0) j rw [hnorm, mul_one] _ ≤ chi := hcondition -
diagonalizableMatrix_eigenvalue_localizationtheorem — Every prescribed eigenvalue of a nearby explicitly diagonalized matrix lies within chi * delta of some eigenvalue of the reference diagonalization. Under the listed assumptions, the stated conclusion follows.hypothesesn :ℕNeZero nvalues values' :Fin n → ℝchi delta :ℝhS :IsUnit S.dethS' :IsUnit S'.dethcondition :squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chihclose :≤ deltaj' :conclusion∃ j, |values' j' - values j| ≤ chi * deltaProof (Lean source)
-- Proof route: take the corresponding nonzero column of `S'` as an eigenvector of the -- perturbed matrix, conjugate its residual by `S⁻¹`, choose a largest coordinate, and compare -- that coordinate against the Euclidean norm. This is the finite-dimensional Bauer--Fike -- argument and uses no normality assumption. theorem diagonalizableMatrix_eigenvalue_localization {n : ℕ} [NeZero n] (S S' : Matrix (Fin n) (Fin n) ℝ) (values values' : Fin n → ℝ) {chi delta : ℝ} (hS : IsUnit S.det) (hS' : IsUnit S'.det) (hcondition : squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi) (hclose : squareOperatorNorm (diagonalizableMatrix S' values' - diagonalizableMatrix S values) ≤ delta) : ∀ j', ∃ j, |values' j' - values j| ≤ chi * delta := by classical intro j' obtain ⟨j, _, hj⟩ := Finset.exists_min_image univ (fun k => |values' j' - values k|) Finset.univ_nonempty refine ⟨j, ?_⟩ let v : Fin n → ℝ := S'.col j' let x : Fin n → ℝ := (S⁻¹).mulVec v have hv_ne : v ≠ 0 := by intro hv apply hS'.ne_zero apply Matrix.det_eq_zero_of_column_eq_zero j' intro i exact congrFun hv i have hv_recover : S.mulVec x = v := by simp [x, Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv S hS] have hx_ne : x ≠ 0 := by intro hx apply hv_ne rw [← hv_recover, hx, Matrix.mulVec_zero] have hinvcol : (S'⁻¹).mulVec v = single j' 1 := by rw [show v = S'.mulVec (single j' 1) by simp [v]] rw [Matrix.mulVec_mulVec, Matrix.nonsing_inv_mul S' hS', Matrix.one_mulVec] have heigen : (diagonalizableMatrix S' values').mulVec v = values' j' • v := by calc _ = S'.mulVec ((diagonal values').mulVec ((S'⁻¹).mulVec v)) := by rw [diagonalizableMatrix, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec] _ = S'.mulVec ((diagonal values').mulVec (single j' 1)) := by rw [hinvcol] _ = S'.mulVec (values' j' • single j' 1) := by congr 1 ext k by_cases hk : k = j' · subst k simp [Matrix.mulVec_diagonal] · simp [Matrix.mulVec_diagonal, hk] _ = values' j' • S'.mulVec (single j' 1) := Matrix.mulVec_smul S' (values' j') (single j' (1 : ℝ)) _ = values' j' • v := by rw [Matrix.mulVec_single_one] have hreference : (diagonalizableMatrix S values).mulVec v = S.mulVec ((diagonal values).mulVec x) := by rw [diagonalizableMatrix, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec] let E := diagonalizableMatrix S' values' - diagonalizableMatrix S values let d : Fin n → ℝ := fun k => values' j' - values k have hcancel (z : Fin n → ℝ) : (S⁻¹).mulVec (S.mulVec z) = z := by rw [Matrix.mulVec_mulVec, Matrix.nonsing_inv_mul S hS, Matrix.one_mulVec] have hres : (diagonal d).mulVec x = (S⁻¹).mulVec (E.mulVec v) := by rw [show E = diagonalizableMatrix S' values' - diagonalizableMatrix S values by rfl] rw [Matrix.sub_mulVec, heigen, hreference, Matrix.mulVec_sub, Matrix.mulVec_smul] change (diagonal d).mulVec x = values' j' • x - (S⁻¹).mulVec (S.mulVec ((diagonal values).mulVec x)) rw [hcancel] ext k simp [d, Matrix.mulVec_diagonal] ring have hlower : |values' j' - values j| * ‖WithLp.toLp 2 x‖ ≤ ‖WithLp.toLp 2 ((diagonal d).mulVec x)‖ := by apply min_abs_mul_euclidean_norm_le_diagonal_mulVec_norm d x j intro k exact hj k (Finset.mem_univ k) have hu1 : ‖WithLp.toLp 2 ((diagonal d).mulVec x)‖ ≤ ‖S⁻¹‖ * ‖WithLp.toLp 2 (E.mulVec v)‖ := by rw [hres] exact Matrix.l2_opNorm_mulVec S⁻¹ (toLp 2 (E.mulVec v)) have hu2 : ‖WithLp.toLp 2 (E.mulVec v)‖ ≤ ‖E‖ * ‖WithLp.toLp 2 v‖ := Matrix.l2_opNorm_mulVec E (toLp 2 v) have hvnorm : ‖WithLp.toLp 2 v‖ ≤ ‖S‖ * ‖WithLp.toLp 2 x‖ := by rw [← hv_recover] exact Matrix.l2_opNorm_mulVec S (toLp 2 x) have hxnorm_pos : 0 < ‖WithLp.toLp 2 x‖ := norm_pos_iff.mpr (by exact fun hx => hx_ne (WithLp.toLp_injective 2 hx)) have hE : ‖E‖ ≤ delta := by rw [← Matrix.l2_opNorm_toEuclideanCLM] simpa [E, squareOperatorNorm] using hclose have hdelta : 0 ≤ delta := (norm_nonneg E).trans hE have hcond : ‖S‖ * ‖S⁻¹‖ ≤ chi := by simpa only [squareOperatorNorm, Matrix.l2_opNorm_toEuclideanCLM] using hcondition have hupper : ‖WithLp.toLp 2 ((diagonal d).mulVec x)‖ ≤ (chi * delta) * ‖WithLp.toLp 2 x‖ := by calc _ ≤ ‖S⁻¹‖ * ‖WithLp.toLp 2 (E.mulVec v)‖ := hu1 _ ≤ ‖S⁻¹‖ * (‖E‖ * ‖WithLp.toLp 2 v‖) := mul_le_mul_of_nonneg_left hu2 (norm_nonneg _) _ ≤ ‖S⁻¹‖ * (delta * ‖WithLp.toLp 2 v‖) := by gcongr _ ≤ ‖S⁻¹‖ * (delta * (‖S‖ * ‖WithLp.toLp 2 x‖)) := by gcongr _ = ((‖S‖ * ‖S⁻¹‖) * delta) * ‖WithLp.toLp 2 x‖ := by ring _ ≤ (chi * delta) * ‖WithLp.toLp 2 x‖ := by gcongr exact le_of_mul_le_mul_right (hlower.trans hupper) hxnorm_pos
Pencil 3 core · 3 supporting This module packages the finite-dimensional inverse perturbation estimates needed after tensor contractions are compressed to the lifted signal space. ★ rightPencil_perturbation_bound
Inverse and tensor-pencil perturbation bounds
This module packages the finite-dimensional inverse perturbation estimates needed after tensor contractions are compressed to the lifted signal space. The constants are exposed separately so applications can assemble a local radius without unfolding proofs.
def rightPencil reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The right generalized-eigenvalue pencil formed from a numerator and denominator matrix. With its explicit inputs, the defined object is given by the displayed formula.
def pencilPerturbationConstant reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The explicit Lipschitz coefficient for a right pencil whose denominator has lower singular value eta and whose numerator norm is at most n * Lambda. The formula is unguarded: it is a Lipschitz coefficient only for positive eta, and eta = 0 gives zero by the division-by-zero convention. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
n :
ℕ
eta Lambda :
ℝ
def
pencilPerturbationConstant n eta Lambda :
ℝ
given by
2 / eta + 2 * n * Lambda / eta ^ 2
theorem rightPencil_perturbation_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Given reference and perturbed numerator and denominator contractions, a positive denominator margin, nonnegative numerator and error bounds, a denominator singular-value bound, a numerator norm bound, numerator and denominator perturbation bounds, and a small-error condition, both denominator matrices are invertible and the two right generalized-eigenvalue pencils differ by the explicit Lipschitz bound. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
n :
ℕ
NeZero n
eta Lambda e :
ℝ
heta :
0 < eta
hLambda :
0 ≤ Lambda
he :
0 ≤ e
hsv :
eta ≤ leastColumnSingularValue Au
hnumer :
squareOperatorNorm Aw ≤ n * Lambda
hnumPert :
squareOperatorNorm (Aw' - Aw) ≤ e
hdenPert :
squareOperatorNorm (Au' - Au) ≤ e
hsmall :
e < eta / 2
conclusion
conclusion 1
IsUnit Au.det
conclusion 2
IsUnit Au'.det
conclusion 3
≤ pencilPerturbationConstant n eta Lambda * e
Proof (Lean source)
-- Proof route: add and subtract `Aw * Au'⁻¹`, then combine the numerator perturbation with the
-- inverse-difference bound and `‖Aw‖ ≤ n Lambda`; use `Matrix.l2_opNorm_mul` throughout.
theorem rightPencil_perturbation_bound {n : ℕ} [NeZero n]
(Aw Au Aw' Au' : Matrix (Fin n) (Fin n) ℝ) {eta Lambda e : ℝ}
(heta : 0 < eta) (hLambda : 0 ≤ Lambda) (he : 0 ≤ e)
(hsv : eta ≤ leastColumnSingularValue Au)
(hnumer : squareOperatorNorm Aw ≤ n * Lambda)
(hnumPert : squareOperatorNorm (Aw' - Aw) ≤ e)
(hdenPert : squareOperatorNorm (Au' - Au) ≤ e)
(hsmall : e < eta / 2) :
IsUnit Au.det ∧ IsUnit Au'.det ∧
squareOperatorNorm (rightPencil Aw' Au' - rightPencil Aw Au) ≤
pencilPerturbationConstant n eta Lambda * e := by
obtain ⟨hdetAu, _⟩ := inverse_operatorNorm_le_reciprocal Au heta hsv
obtain ⟨hdetAu', hinvAu', hdiffInv⟩ :=
inverse_perturbation_bound Au Au' heta he hsv hdenPert hsmall
change ‖Aw‖ ≤ n * Lambda at hnumer
change ‖Aw' - Aw‖ ≤ e at hnumPert
change ‖Au'⁻¹‖ ≤ 2 / eta at hinvAu'
change ‖Au'⁻¹ - Au⁻¹‖ ≤ 2 * e / eta ^ 2 at hdiffInv
refine ⟨hdetAu, hdetAu', ?_⟩
change ‖Aw' * Au'⁻¹ - Aw * Au⁻¹‖ ≤
(2 / eta + 2 * n * Lambda / eta ^ 2) * e
have hsplit : Aw' * Au'⁻¹ - Aw * Au⁻¹ =
(Aw' - Aw) * Au'⁻¹ + Aw * (Au'⁻¹ - Au⁻¹) := by
noncomm_ring
rw [hsplit]
calc
‖(Aw' - Aw) * Au'⁻¹ + Aw * (Au'⁻¹ - Au⁻¹)‖ ≤
‖(Aw' - Aw) * Au'⁻¹‖ + ‖Aw * (Au'⁻¹ - Au⁻¹)‖ := norm_add_le _ _
_ ≤ ‖Aw' - Aw‖ * ‖Au'⁻¹‖ + ‖Aw‖ * ‖Au'⁻¹ - Au⁻¹‖ :=
add_le_add (Matrix.l2_opNorm_mul _ _) (Matrix.l2_opNorm_mul _ _)
_ ≤ e * (2 / eta) + (n * Lambda) * (2 * e / eta ^ 2) := by
apply add_le_add
· exact mul_le_mul hnumPert hinvAu' (norm_nonneg _)
he
· exact mul_le_mul hnumer hdiffInv (norm_nonneg _)
(mul_nonneg (Nat.cast_nonneg n) hLambda)
_ = (2 / eta + 2 * n * Lambda / eta ^ 2) * e := by ring
3 supporting declarations (lemmas, instances)
-
inverse_operatorNorm_le_reciprocaltheorem — A positive lower bound on the least singular value of a real square matrix makes its determinant a unit and bounds the operator norm of its inverse by the reciprocal margin. Under the listed assumptions, the stated conclusion follows.hypothesesProof (Lean source)
-- Proof route: diagonalize `A†A`; positivity of its last eigenvalue eliminates the kernel and -- gives the inverse bound after applying the least-singular-value expansion inequality. The -- preceding module already contains the required ingredients: -- `injective_of_pos_le_leastColumnSingularValue`, `Matrix.mulVec_injective_iff_isUnit`, and the -- proof pattern of `squareInverse_operatorNorm_le_reciprocal`. theorem inverse_operatorNorm_le_reciprocal {n : ℕ} [NeZero n] (A : Matrix (Fin n) (Fin n) ℝ) {eta : ℝ} (heta : 0 < eta) (hsv : eta ≤ leastColumnSingularValue A) : IsUnit A.det ∧ squareOperatorNorm A⁻¹ ≤ eta⁻¹ := by have hinj := injective_of_pos_le_leastColumnSingularValue A heta hsv have hmulVec : Injective A.mulVec := by intro x y hxy have hlp : A.toEuclideanLin (toLp 2 x) = A.toEuclideanLin (toLp 2 y) := by simpa [Matrix.toEuclideanLin_apply] using congrArg (toLp 2) hxy have := hinj hlp simpa using congrArg WithLp.ofLp this have hunitA : IsUnit A := Matrix.mulVec_injective_iff_isUnit.mp hmulVec have hdet : IsUnit A.det := (Matrix.isUnit_iff_isUnit_det A).mp hunitA refine ⟨hdet, ?_⟩ rw [squareOperatorNorm] apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr heta.le) intro x let E := (Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ)) have hcancel : E A (E A⁻¹ x) = x := by rw [← ContinuousLinearMap.mul_apply, ← map_mul, Matrix.mul_nonsing_inv A hdet, map_one, ContinuousLinearMap.one_apply] have hleast := least_singularValue_mul_norm_le A.toEuclideanLin hinj (E A⁻¹ x) have heta_mul : eta * ‖E A⁻¹ x‖ ≤ ‖x‖ := by calc eta * ‖E A⁻¹ x‖ ≤ leastColumnSingularValue A * ‖E A⁻¹ x‖ := mul_le_mul_of_nonneg_right hsv (norm_nonneg _) _ ≤ ‖A.toEuclideanLin (E A⁻¹ x)‖ := by simpa [leastColumnSingularValue, finrank_euclideanSpace] using hleast _ = ‖x‖ := by change ‖E A (E A⁻¹ x)‖ = ‖x‖ rw [hcancel] rw [inv_mul_eq_div] exact (le_div_iff₀ heta).2 (by simpa [mul_comm] using heta_mul) -
inverse_perturbation_boundtheorem — If a square matrix with least singular value at least eta is perturbed by at most e < eta / 2, the perturbed matrix stays invertible and its inverse norm is at most 2 / eta. Under the listed assumptions, the stated conclusion follows.hypothesesn :ℕNeZero neta e :ℝheta :0 < etahe :0 ≤ ehsv :eta ≤ leastColumnSingularValue Ahpert :squareOperatorNorm (A' - A) ≤ ehsmall :e < eta / 2conclusionconclusion 1IsUnit A'.detconclusion 2squareOperatorNorm A'⁻¹ ≤ 2 / etaconclusion 3squareOperatorNorm (A'⁻¹ - A⁻¹) ≤ 2 * e / eta ^ 2Proof (Lean source)
-- Proof route: turn the determinant-unit witness for `A` into a matrix unit and use -- `Units.ofNearby`/`Units.val_ofNearby` after proving -- `‖A' - A‖ < ‖A⁻¹‖⁻¹`. Bound the new inverse by factoring through the inverse of -- `1 + A⁻¹(A'-A)` (or its geometric series), then use `Matrix.inv_sub_inv` for -- `A'⁻¹-A⁻¹ = A'⁻¹(A-A')A⁻¹`. theorem inverse_perturbation_bound {n : ℕ} [NeZero n] (A A' : Matrix (Fin n) (Fin n) ℝ) {eta e : ℝ} (heta : 0 < eta) (he : 0 ≤ e) (hsv : eta ≤ leastColumnSingularValue A) (hpert : squareOperatorNorm (A' - A) ≤ e) (hsmall : e < eta / 2) : IsUnit A'.det ∧ squareOperatorNorm A'⁻¹ ≤ 2 / eta ∧ squareOperatorNorm (A'⁻¹ - A⁻¹) ≤ 2 * e / eta ^ 2 := by obtain ⟨hdetA, hinvA⟩ := inverse_operatorNorm_le_reciprocal A heta hsv change ‖A⁻¹‖ ≤ eta⁻¹ at hinvA change ‖A' - A‖ ≤ e at hpert let D := A' - A let Q := A⁻¹ * D have hQ : ‖Q‖ < 1 / 2 := by calc ‖Q‖ ≤ ‖A⁻¹‖ * ‖D‖ := Matrix.l2_opNorm_mul _ _ _ ≤ eta⁻¹ * e := mul_le_mul hinvA hpert (norm_nonneg _) (inv_nonneg.mpr heta.le) _ < 1 / 2 := by rw [inv_mul_eq_div, div_lt_iff₀ heta] simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using hsmall have hnegQ : ‖-Q‖ < 1 := by simpa using hQ.trans (by norm_num) let B : Matrix (Fin n) (Fin n) ℝ := 1 + Q have hdetB : IsUnit B.det := by apply (Matrix.isUnit_iff_isUnit_det B).mp have hu := (Units.oneSub (-Q) hnegQ).isUnit simpa [B] using hu have hfactor : A' = A * B := by calc A' = A + D := by simp [D] _ = A * (1 + Q) := by simp only [Matrix.mul_add, Matrix.mul_one, Q, D] rw [← Matrix.mul_assoc, Matrix.mul_nonsing_inv A hdetA, Matrix.one_mul] _ = A * B := rfl have hdetA' : IsUnit A'.det := by rw [hfactor, Matrix.det_mul] exact hdetA.mul hdetB have hinvB : ‖B⁻¹‖ ≤ 2 := by rw [Matrix.nonsing_inv_eq_ringInverse] rw [show B = 1 - (-Q) by simp [B], NormedRing.inverse_one_sub (-Q) hnegQ] change ‖∑' k : ℕ, (-Q) ^ k‖ ≤ 2 have hgeom := tsum_geometric_le_of_norm_lt_one (-Q) hnegQ have hden : (1 - ‖-Q‖)⁻¹ ≤ 2 := by have : ‖-Q‖ < 1 / 2 := by simpa using hQ exact inv_le_of_inv_le₀ (by norm_num) (by norm_num; linarith) have hgeom' : ‖∑' k : ℕ, (-Q) ^ k‖ ≤ (1 - ‖-Q‖)⁻¹ := by simpa only [norm_one, sub_self, zero_add] using hgeom exact hgeom'.trans hden have hinvA' : ‖A'⁻¹‖ ≤ 2 / eta := by rw [hfactor, Matrix.mul_inv_rev] calc ‖B⁻¹ * A⁻¹‖ ≤ ‖B⁻¹‖ * ‖A⁻¹‖ := Matrix.l2_opNorm_mul _ _ _ ≤ 2 * eta⁻¹ := mul_le_mul hinvB hinvA (norm_nonneg _) (by norm_num) _ = 2 / eta := by rw [div_eq_mul_inv] refine ⟨hdetA', hinvA', ?_⟩ change ‖A'⁻¹ - A⁻¹‖ ≤ 2 * e / eta ^ 2 have hunitA' : IsUnit A' := (Matrix.isUnit_iff_isUnit_det A').2 hdetA' have hunitA : IsUnit A := (Matrix.isUnit_iff_isUnit_det A).2 hdetA rw [Matrix.inv_sub_inv ⟨fun _ => hunitA, fun _ => hunitA'⟩] calc ‖A'⁻¹ * (A - A') * A⁻¹‖ ≤ ‖A'⁻¹ * (A - A')‖ * ‖A⁻¹‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖A'⁻¹‖ * ‖A - A'‖) * ‖A⁻¹‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ ≤ ((2 / eta) * e) * eta⁻¹ := by have hdiff : ‖A - A'‖ ≤ e := by simpa [norm_sub_rev] using hpert have hleft : ‖A'⁻¹‖ * ‖A - A'‖ ≤ (2 / eta) * e := mul_le_mul hinvA' hdiff (norm_nonneg _) (div_nonneg (by norm_num) heta.le) exact mul_le_mul hleft hinvA (norm_nonneg _) (mul_nonneg (div_nonneg (by norm_num) heta.le) he) _ = 2 * e / eta ^ 2 := by field_simp [heta.ne'] -
rightPencil_eq_diagonalizationtheorem — Exact contracted factorizations produce a simultaneous diagonalization of every right pencil, with diagonal entries equal to probe-loading ratios. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionrightPencil (S * diagonal (fun j => lam j * num j) * S.transpose) (S * diagonal (fun j => lam j * den j) * S.transpose)= S * diagonal (fun j => num j / den j) * S⁻¹Proof (Lean source)
-- Proof route: use determinant-unit closure for `S`, `S.transpose`, and the nonzero diagonal -- core, expand the nonsingular inverse of a product, cancel `S.transpose`, and check the -- remaining diagonal identity entrywise with `Matrix.diagonal_mul_diagonal`. theorem rightPencil_eq_diagonalization {n : ℕ} (S : Matrix (Fin n) (Fin n) ℝ) (lam den num : Fin n → ℝ) (hS : IsUnit S.det) (hload : ∀ j, lam j * den j ≠ 0) : rightPencil (S * diagonal (fun j => lam j * num j) * S.transpose) (S * diagonal (fun j => lam j * den j) * S.transpose) = S * diagonal (fun j => num j / den j) * S⁻¹ := by let Dnum := diagonal (fun j => lam j * num j) let Dden := diagonal (fun j => lam j * den j) let Drat := diagonal (fun j => num j / den j) have hSt : IsUnit S.transpose.det := Matrix.isUnit_det_transpose S hS have hdiag : Dnum * Dden⁻¹ = Drat := by let f : Fin n → ℝ := fun j => lam j * den j have hf : IsUnit f := Pi.isUnit_iff.mpr fun j => isUnit_iff_ne_zero.mpr (hload j) obtain ⟨u, hu⟩ := hf have hinvf : Ring.inverse f = ↑u⁻¹ := by rw [← hu, Ring.inverse_unit] rw [Matrix.inv_diagonal, Matrix.diagonal_mul_diagonal] congr 1 funext j have hlam : lam j ≠ 0 := left_ne_zero_of_mul (hload j) have hden : den j ≠ 0 := right_ne_zero_of_mul (hload j) have hcancel : f j * Ring.inverse f j = 1 := by rw [hinvf, ← hu] exact congrFun u.val_inv j have hinv_entry : Ring.inverse f j = (f j)⁻¹ := by apply mul_left_cancel₀ (hload j) rw [hcancel, mul_inv_cancel₀ (hload j)] change lam j * num j * Ring.inverse f j = num j / den j rw [hinv_entry] dsimp only [f] field_simp [hlam, hden] change (S * Dnum * S.transpose) * (S * Dden * S.transpose)⁻¹ = S * Drat * S⁻¹ rw [Matrix.mul_inv_rev, Matrix.mul_inv_rev] simp only [Matrix.mul_assoc] rw [← Matrix.mul_assoc S.transpose S.transpose⁻¹, Matrix.mul_nonsing_inv S.transpose hSt, Matrix.one_mul] rw [← Matrix.mul_assoc Dnum Dden⁻¹, hdiag]
Recovery 7 core · 6 supporting This module turns matched spectral projectors into quantitative direction information. ★ traceCoordinates_perturbation_bound
Recovery and normalization of directions
This module turns matched spectral projectors into quantitative direction information. It includes both direct recovery of a rank-one lifted line from a nearby projector and the trace-coordinate construction that removes the degree-lift ambiguity by using coordinate probes.
def standardBasis reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The standard coordinate vector in a finite real coordinate space. With its explicit inputs, the defined object is given by the displayed formula.
def normalizeFinite reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Normalize a finite real array by its Euclidean norm, with the conventional zero value when the input is zero. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
z :
ι → ℝ
def
normalizeFinite z :
ι → ℝ
given by
(finiteFrobeniusNorm z)⁻¹ • z
def normalizeVec reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Normalize a finite coordinate vector by its Euclidean norm, with the conventional zero value when the input is zero. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def recoverRankOneLift reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Apply a candidate projector to a degree-d rank-one lift and normalize the resulting lifted direction. With its explicit inputs, the defined object is given by the displayed formula.
def traceCoordinates reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Trace coordinates evaluate each coordinate pencil against the j-th matrix of a supplied matrix family, by the trace of their product. No condition is imposed on the family; in the recovery argument it is a family of rank-one spectral projectors. With its explicit inputs, the defined object is given by the displayed formula.
theorem traceCoordinates_perturbation_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Given reference and perturbed coordinate pencils, reference and perturbed matrix families (arbitrary matrices; projectors in the intended use), coordinate-pencil error bounds, projector error bounds, perturbed-projector norm bounds, and reference-pencil norm bounds, every trace coordinate obeys the explicit product error bound. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
p n :
ℕ
pencilError projectorError projectorNorm pencilNorm :
ℝ
hpencil :
hprojector :
∀ j, squareOperatorNorm (P' j - P j) ≤ projectorError
hprojectorNorm :
∀ j, squareOperatorNorm (P' j) ≤ projectorNorm
hpencilNorm :
∀ i, squareOperatorNorm (G (standardBasis p i)) ≤ pencilNorm
i j :
conclusion
|traceCoordinates G' P' j i - traceCoordinates G P j i|
≤ n * (pencilError * projectorNorm + pencilNorm * projectorError)
Proof (Lean source)
-- Proof route: write `G'P'-GP = (G'-G)P' + G(P'-P)`, use submultiplicativity, and finish with
-- `abs_trace_le_card_mul_operatorNorm`.
theorem traceCoordinates_perturbation_bound {p n : ℕ}
(G G' : Vec p → Matrix (Fin n) (Fin n) ℝ)
(P P' : Fin n → Matrix (Fin n) (Fin n) ℝ)
{pencilError projectorError projectorNorm pencilNorm : ℝ}
(hpencil : ∀ i, squareOperatorNorm
(G' (standardBasis p i) - G (standardBasis p i)) ≤ pencilError)
(hprojector : ∀ j, squareOperatorNorm (P' j - P j) ≤ projectorError)
(hprojectorNorm : ∀ j, squareOperatorNorm (P' j) ≤ projectorNorm)
(hpencilNorm : ∀ i, squareOperatorNorm (G (standardBasis p i)) ≤ pencilNorm) :
∀ i j, |traceCoordinates G' P' j i - traceCoordinates G P j i| ≤
n * (pencilError * projectorNorm + pencilNorm * projectorError) := by
classical
intro i j
let e := standardBasis p i
have hpencilError : 0 ≤ pencilError :=
(show 0 ≤ squareOperatorNorm (G' e - G e) by
exact norm_nonneg _).trans (hpencil i)
have hprojectorError : 0 ≤ projectorError :=
(show 0 ≤ squareOperatorNorm (P' j - P j) by
exact norm_nonneg _).trans (hprojector j)
have hprojectorNorm₀ : 0 ≤ projectorNorm :=
(show 0 ≤ squareOperatorNorm (P' j) by
exact norm_nonneg _).trans (hprojectorNorm j)
have hpencilNorm₀ : 0 ≤ pencilNorm :=
(show 0 ≤ squareOperatorNorm (G e) by
exact norm_nonneg _).trans (hpencilNorm i)
have hdecomp :
G' e * P' j - G e * P j =
(G' e - G e) * P' j + G e * (P' j - P j) := by
noncomm_ring
have hop : squareOperatorNorm (G' e * P' j - G e * P j) ≤
pencilError * projectorNorm + pencilNorm * projectorError := by
rw [hdecomp]
calc
squareOperatorNorm ((G' e - G e) * P' j + G e * (P' j - P j)) ≤
squareOperatorNorm ((G' e - G e) * P' j) +
squareOperatorNorm (G e * (P' j - P j)) :=
squareOperatorNorm_add_le _ _
_ ≤ squareOperatorNorm (G' e - G e) * squareOperatorNorm (P' j) +
squareOperatorNorm (G e) * squareOperatorNorm (P' j - P j) :=
add_le_add (squareOperatorNorm_mul_le _ _) (squareOperatorNorm_mul_le _ _)
_ ≤ pencilError * projectorNorm + pencilNorm * projectorError := by
apply add_le_add
· exact mul_le_mul (hpencil i) (hprojectorNorm j)
(show 0 ≤ squareOperatorNorm (P' j) by exact norm_nonneg _) hpencilError
· exact mul_le_mul (hpencilNorm i) (hprojector j)
(show 0 ≤ squareOperatorNorm (P' j - P j) by exact norm_nonneg _)
hpencilNorm₀
change |trace (G' e * P' j) - trace (G e * P j)| ≤ _
rw [← Matrix.trace_sub]
exact (abs_trace_le_card_mul_operatorNorm (G' e * P' j - G e * P j)).trans
(mul_le_mul_of_nonneg_left hop (Nat.cast_nonneg n))
def permuteColumns reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Permute the columns of a finite factor matrix. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
def
given by
fun i j => C i (pi j)
6 supporting declarations (lemmas, instances)
-
recoverRankOneLift_error_letheorem — A matched nearby projector recovers the normalized rank-one lifted direction with error at most 2 * delta / (1 - delta). Under the listed assumptions, the stated conclusion follows.hypothesesp d :ℕhd :0 < dc :Vec pdelta :ℝhunit :finiteFrobeniusNorm c = 1hfixed :P.mulVec (fun I => ∏ k, c (I k)) = fun I => ∏ k, c (I k)hdelta :0 ≤ deltahsmall :delta < 1hclose :squareOperatorNorm (P' - P) ≤ deltaconclusionfiniteFrobeniusNorm (recoverRankOneLift P' c - fun I => ∏ k, c (I k))≤ 2 * delta / (1 - delta)Proof (Lean source)
-- Proof route: apply the operator bound to the unit true lift, deduce that its projected image -- has norm at least `1-delta`, and use `normalizeFinite_sub_normalizeFinite_le`. theorem recoverRankOneLift_error_le {p d : ℕ} (hd : 0 < d) (P P' : Matrix (LiftIndex p d) (LiftIndex p d) ℝ) (c : Vec p) {delta : ℝ} (hunit : finiteFrobeniusNorm c = 1) (hfixed : P.mulVec (fun I => ∏ k, c (I k)) = fun I => ∏ k, c (I k)) (hdelta : 0 ≤ delta) (hsmall : delta < 1) (hclose : squareOperatorNorm (P' - P) ≤ delta) : finiteFrobeniusNorm (recoverRankOneLift P' c - fun I => ∏ k, c (I k)) ≤ 2 * delta / (1 - delta) := by classical let v : LiftIndex p d → ℝ := fun I => ∏ k, c (I k) let C₁ : FactorMatrix p 1 := fun i _ => c i have hC₁ : ∀ j, finiteFrobeniusNorm (C₁.col j) = 1 := by intro j change finiteFrobeniusNorm (fun i => c i) = 1 exact hunit have hv : finiteFrobeniusNorm v = 1 := by have h := finiteFrobeniusNorm_liftedColumn_eq_one hd C₁ hC₁ (0 : Fin 1) change finiteFrobeniusNorm (fun I : LiftIndex p d => ∏ k, c (I k)) = 1 at h exact h have herrEq : P'.mulVec v - v = (P' - P).mulVec v := by rw [Matrix.sub_mulVec, hfixed] have herr : finiteFrobeniusNorm (P'.mulVec v - v) ≤ delta := by rw [herrEq] calc finiteFrobeniusNorm ((P' - P).mulVec v) ≤ squareOperatorNorm (P' - P) * finiteFrobeniusNorm v := finiteFrobeniusNorm_mulVec_le _ _ _ ≤ delta * 1 := mul_le_mul hclose hv.le (Real.sqrt_nonneg _) hdelta _ = delta := mul_one _ have hlower : 1 - delta ≤ finiteFrobeniusNorm (P'.mulVec v) := by have hrev := abs_finiteFrobeniusNorm_sub_le (P'.mulVec v) v rw [hv] at hrev have hsigned : 1 - finiteFrobeniusNorm (P'.mulVec v) ≤ |finiteFrobeniusNorm (P'.mulVec v) - 1| := by rw [abs_sub_comm] exact le_abs_self _ linarith have hpos : 0 < finiteFrobeniusNorm (P'.mulVec v) := (sub_pos.mpr hsmall).trans_le hlower have hnormv : normalizeFinite v = v := by simp [normalizeFinite, hv] have hgeneric := normalizeFinite_sub_normalizeFinite_le (P'.mulVec v) v hpos (by rw [hv]; norm_num) rw [hnormv] at hgeneric change finiteFrobeniusNorm (recoverRankOneLift P' c - v) ≤ _ rw [recoverRankOneLift] change finiteFrobeniusNorm (normalizeFinite (P'.mulVec v) - v) ≤ _ calc finiteFrobeniusNorm (normalizeFinite (P'.mulVec v) - v) ≤ 2 * finiteFrobeniusNorm (P'.mulVec v - v) / min (finiteFrobeniusNorm (P'.mulVec v)) (finiteFrobeniusNorm v) := hgeneric _ ≤ 2 * delta / (1 - delta) := by have hden : 1 - delta ≤ min (finiteFrobeniusNorm (P'.mulVec v)) (finiteFrobeniusNorm v) := by rw [hv] exact le_min hlower (by linarith) have hdenpos : 0 < min (finiteFrobeniusNorm (P'.mulVec v)) (finiteFrobeniusNorm v) := (sub_pos.mpr hsmall).trans_le hden exact div_le_div₀ (by positivity) (mul_le_mul_of_nonneg_left herr (by norm_num)) (sub_pos.mpr hsmall) hden -
traceCoordinates_diagonalizationtheorem — For an exact simultaneous diagonalization, trace coordinates recover a factor column divided by its positive denominator-probe loading. Under the listed assumptions, the stated conclusion follows.hypothesesconclusiontraceCoordinates (fun w => diagonalizableMatrix S (fun j => dot w (C.col j) / dot u (C.col j))) (coordinateProjector S)= fun j => (dot u (C.col j))⁻¹ • C.col jProof (Lean source)
theorem traceCoordinates_diagonalization {p n : ℕ} (C : FactorMatrix p n) (u : Vec p) (S : Matrix (Fin n) (Fin n) ℝ) (hS : IsUnit S.det) (hprobe : ∀ j, dot u (C.col j) ≠ 0) : traceCoordinates (fun w => diagonalizableMatrix S (fun j => dot w (C.col j) / dot u (C.col j))) (coordinateProjector S) = fun j => (dot u (C.col j))⁻¹ • C.col j := by classical funext j i rw [traceCoordinates, trace_diagonalizableMatrix_mul_coordinateProjector S hS] have hcoord : dot (standardBasis p i) (C.col j) = C i j := by simp [dot, standardBasis] rw [hcoord] simp only [Pi.smul_apply, smul_eq_mul, Matrix.col_apply] field_simp [hprobe j] -
finiteFrobeniusNorm_sub_le_sqrt_multheorem — A uniform coordinatewise error bound gives a Euclidean error bound larger by at most the square root of the number of coordinates. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionfiniteFrobeniusNorm (x - y) ≤ sqrt p * bProof (Lean source)
theorem finiteFrobeniusNorm_sub_le_sqrt_mul {p : ℕ} (x y : Vec p) {b : ℝ} (hb : 0 ≤ b) (hcoord : ∀ i, |x i - y i| ≤ b) : finiteFrobeniusNorm (x - y) ≤ sqrt p * b := by have hsum : ∑ i, (x i - y i) ^ 2 ≤ p * b ^ 2 := by calc ∑ i, (x i - y i) ^ 2 ≤ ∑ _i : Fin p, b ^ 2 := by apply Finset.sum_le_sum intro i _ rw [← sq_abs] exact (sq_le_sq₀ (abs_nonneg _) hb).2 (hcoord i) _ = p * b ^ 2 := by simp apply (sq_le_sq₀ (Real.sqrt_nonneg _) (mul_nonneg (Real.sqrt_nonneg _) hb)).mp rw [Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _), mul_pow, Real.sq_sqrt (Nat.cast_nonneg p)] simpa only [Pi.sub_apply] using hsum -
normalizeVec_sub_normalizeVec_letheorem — Normalization is quantitatively stable away from zero: the distance between normalized vectors is at most twice their original distance divided by the smaller input norm. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionProof (Lean source)
theorem normalizeVec_sub_normalizeVec_le {p : ℕ} (x y : Vec p) (hx : 0 < finiteFrobeniusNorm x) (hy : 0 < finiteFrobeniusNorm y) : finiteFrobeniusNorm (normalizeVec x - normalizeVec y) ≤ 2 * finiteFrobeniusNorm (x - y) / min (finiteFrobeniusNorm x) (finiteFrobeniusNorm y) := by simpa only [normalizeVec] using normalizeFinite_sub_normalizeFinite_le x y hx hy -
normalizeVec_inv_smul_eqtheorem — Positively rescaling a unit vector and then normalizing returns the original vector. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionnormalizeVec (a⁻¹ • c) = cProof (Lean source)
-- Proof route: compute the squared Frobenius norm of `a⁻¹ • c`, use positivity of `a` to -- simplify `|a⁻¹|`, then unfold normalization and cancel the nonzero scale. theorem normalizeVec_inv_smul_eq {p : ℕ} (c : Vec p) (a : ℝ) (hc : finiteFrobeniusNorm c = 1) (ha : 0 < a) : normalizeVec (a⁻¹ • c) = c := by have hscale : finiteFrobeniusNorm (a⁻¹ • c) = a⁻¹ := by rw [finiteFrobeniusNorm_smul, hc, mul_one, abs_of_pos (inv_pos.mpr ha)] ext i simp [normalizeVec, normalizeFinite, hscale, ha.ne'] -
matrixFrobeniusNorm_le_sqrt_mul_of_columnstheorem — If corresponding columns have Euclidean error at most b, their matrix Frobenius error is at most sqrt n * b. Under the listed assumptions, the stated conclusion follows.hypothesesp n :ℕA B :FactorMatrix p nb :ℝhb :0 ≤ bhcol :∀ j, finiteFrobeniusNorm (A.col j - B.col j) ≤ bconclusionmatrixFrobeniusNorm (A - B) ≤ sqrt n * bProof (Lean source)
-- Proof route: unfold the matrix norm, regroup the entry sum by columns, square every column -- bound, sum, and use `Real.sqrt_le_sqrt` together with `Real.sq_sqrt`. theorem matrixFrobeniusNorm_le_sqrt_mul_of_columns {p n : ℕ} (A B : FactorMatrix p n) {b : ℝ} (hb : 0 ≤ b) (hcol : ∀ j, finiteFrobeniusNorm (A.col j - B.col j) ≤ b) : matrixFrobeniusNorm (A - B) ≤ sqrt n * b := by have hcolSq (j : Fin n) : ∑ i, (A i j - B i j) ^ 2 ≤ b ^ 2 := by have h := (sq_le_sq₀ (Real.sqrt_nonneg _) hb).2 (hcol j) rw [Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] at h simpa only [Matrix.col_apply, Pi.sub_apply] using h have hsum : ∑ x : Fin p × Fin n, ((A - B) x.1 x.2) ^ 2 ≤ n * b ^ 2 := by rw [Fintype.sum_prod_type, Finset.sum_comm] calc ∑ j : Fin n, ∑ i : Fin p, ((A - B) i j) ^ 2 ≤ ∑ _j : Fin n, b ^ 2 := by apply Finset.sum_le_sum intro j _ simpa only [Matrix.sub_apply] using hcolSq j _ = n * b ^ 2 := by simp apply (sq_le_sq₀ (Real.sqrt_nonneg _) (mul_nonneg (Real.sqrt_nonneg _) hb)).mp change (sqrt (∑ x : Fin p × Fin n, ((A - B) x.1 x.2) ^ 2)) ^ 2 ≤ (sqrt n * b) ^ 2 rw [Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _), mul_pow, Real.sq_sqrt (Nat.cast_nonneg n)] exact hsum
Conditioning 3 core · 8 supporting This module records how an orthonormal basis of the lifted column space preserves the signal singular values. ★ compressedDenominator_leastSingularValue
Conditioning of compressed lifted factors
This module records how an orthonormal basis of the lifted column space preserves the signal singular values. It then derives explicit lower and upper bounds for the contracted matrices which form the denominator and numerators of a tensor pencil.
def OrthonormalColumns reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
A finite matrix has orthonormal columns when its transpose times itself is the identity. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def SameColumnSpace reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Two finite matrices have the same column space when their associated Euclidean linear maps have equal ranges. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
ι κ :
U V :
Matrix ι κ ℝ
def
SameColumnSpace U V :
Prop
given by
U.toEuclideanLin.range = V.toEuclideanLin.range
theorem compressedDenominator_leastSingularValue reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Given a factor matrix, its coefficients, a denominator probe, orthonormal lifted coordinates, positive degree and margins, a lifted singular-value margin, coefficient lower bounds, and probe-loading lower bounds, the compressed denominator contraction has least singular value at least the assembled margin. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
p n d q :
ℕ
NeZero n
C :
FactorMatrix p n
lam :
Fin n → ℝ
u :
Vec p
sigma kappa :
ℝ
hq :
0 < q
hsigma :
0 < sigma
hkappa :
0 < kappa
horth :
hspace :
SameColumnSpace U (liftedDirections d C)
hlift :
sigma ≤ leastColumnSingularValue (liftedDirections d C)
hlam :
∀ j, kappa ≤ |lam j|
hprobe :
∀ j, sigma ≤ dot u (C.col j)
conclusion
kappa * sigma ^ (q + 2)
≤ leastColumnSingularValue ((U.transpose * liftedDirections d C) * diagonal (fun j => lam j * dot u (C.col j) ^ q) * (U.transpose * liftedDirections d C).transpose)
Proof (Lean source)
-- Proof route: use `Matrix.singularValues_mul_mul_transpose_lower_bound`; the diagonal core
-- expands by `kappa * sigma^q`, while each compressed lifted factor expands by `sigma`.
theorem compressedDenominator_leastSingularValue {p n d q : ℕ} [NeZero n]
(C : FactorMatrix p n) (lam : Fin n → ℝ) (u : Vec p)
(U : Matrix (LiftIndex p d) (Fin n) ℝ) {sigma kappa : ℝ}
(hq : 0 < q) (hsigma : 0 < sigma) (hkappa : 0 < kappa)
(horth : OrthonormalColumns U)
(hspace : SameColumnSpace U (liftedDirections d C))
(hlift : sigma ≤ leastColumnSingularValue (liftedDirections d C))
(hlam : ∀ j, kappa ≤ |lam j|)
(hprobe : ∀ j, sigma ≤ dot u (C.col j)) :
kappa * sigma ^ (q + 2) ≤ leastColumnSingularValue
((U.transpose * liftedDirections d C) *
diagonal (fun j => lam j * dot u (C.col j) ^ q) *
(U.transpose * liftedDirections d C).transpose) := by
let S := U.transpose * liftedDirections d C
let D := diagonal (fun j => lam j * dot u (C.col j) ^ q)
have hSsv : sigma ≤ leastColumnSingularValue S :=
compressedLift_leastSingularValue C U hsigma hlift horth hspace
have hSinj : Injective S.toEuclideanLin :=
injective_of_pos_le_leastColumnSingularValue S hsigma hSsv
have hload (j : Fin n) : kappa * sigma ^ q ≤
|lam j * dot u (C.col j) ^ q| := by
have huj : 0 < dot u (C.col j) := hsigma.trans_le (hprobe j)
rw [abs_mul, abs_pow, abs_of_pos huj]
exact mul_le_mul (hlam j) (pow_le_pow_left₀ hsigma.le (hprobe j) q)
(pow_nonneg hsigma.le q) (abs_nonneg _)
have hDinj : Injective D.toEuclideanLin := by
intro x y hxy
apply PiLp.ext
intro j
have hj := congrArg
(fun z : EuclideanSpace ℝ (Fin n) => ofLp z j) hxy
simp only [D, Matrix.toEuclideanLin_apply, WithLp.ofLp_toLp,
Matrix.mulVec_diagonal] at hj
have hne : lam j * dot u (C.col j) ^ q ≠ 0 := by
intro hz
have := hload j
rw [hz, abs_zero] at this
have hcpos : 0 < kappa * sigma ^ q :=
mul_pos hkappa (pow_pos hsigma q)
linarith
exact mul_left_cancel₀ hne hj
have hDsv : kappa * sigma ^ q ≤ leastColumnSingularValue D := by
apply le_singularValues_of_subspace
D.toEuclideanLin ⊤
· exact mul_nonneg hkappa.le (pow_nonneg hsigma.le q)
· simp only [finrank_euclideanSpace, finrank_top]
exact sub_lt (Fintype.card_pos) (by omega)
· intro x _hx
apply (sq_le_sq₀
(mul_nonneg (mul_nonneg hkappa.le (pow_nonneg hsigma.le q)) (norm_nonneg x))
(norm_nonneg (D.toEuclideanLin x))).mp
rw [mul_pow, EuclideanSpace.norm_sq_eq, EuclideanSpace.norm_sq_eq,
Finset.mul_sum]
apply Finset.sum_le_sum
intro j _
simp only [D, Matrix.toEuclideanLin_apply, WithLp.ofLp_toLp,
Matrix.mulVec_diagonal, Real.norm_eq_abs, PiLp.inner_apply,
RCLike.inner_apply, conj_trivial, mul_pow]
rw [abs_mul, mul_pow]
convert mul_le_mul_of_nonneg_right
((sq_le_sq₀ (mul_nonneg hkappa.le (pow_nonneg hsigma.le q))
(abs_nonneg _)).2 (hload j)) (sq_nonneg (ofLp x j)) using 1 <;>
simp only [sq_abs] <;> ring
have hprod := singularValues_mul_mul_transpose_lower_bound
S D S hSinj hDinj hSinj
have hS0 := S.toEuclideanLin.singularValues_nonneg (card (Fin n) - 1)
have hD0 := D.toEuclideanLin.singularValues_nonneg (card (Fin n) - 1)
calc
kappa * sigma ^ (q + 2) = sigma * (kappa * sigma ^ q) * sigma := by
rw [pow_add]
ring
_ ≤ leastColumnSingularValue S * leastColumnSingularValue D *
leastColumnSingularValue S := by
exact mul_le_mul
(mul_le_mul hSsv hDsv (mul_nonneg hkappa.le (pow_nonneg hsigma.le q)) hS0)
hSsv hsigma.le (mul_nonneg hS0 hD0)
_ ≤ leastColumnSingularValue (S * D * S.transpose) := by
simpa [leastColumnSingularValue] using hprod
8 supporting declarations (lemmas, instances)
-
leastColumnSingularValue_transpose_mul_eqtheorem — Compressing a full-column-rank matrix in an orthonormal basis of its column space preserves its least column singular value. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionleastColumnSingularValue (U.transpose * V) = leastColumnSingularValue VProof (Lean source)
-- Proof route: turn `U` into a `LinearIsometry` using `UᵀU = I`, rewrite the transpose product -- as composition with that isometry, and apply -- `singularValues_comp_linearIsometry_last` to the adjoint/range equality induced by `hspace`. theorem leastColumnSingularValue_transpose_mul_eq {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] [Nonempty κ] (U V : Matrix ι κ ℝ) (horth : OrthonormalColumns U) (hspace : SameColumnSpace U V) (hinj : Injective V.toEuclideanLin) : leastColumnSingularValue (U.transpose * V) = leastColumnSingularValue V := by let W := orthonormalColumnsLinearIsometry U horth let S := (U.transpose * V).toEuclideanLin let M := V.toEuclideanLin have hS : S = W.toLinearMap.adjoint ∘ₗ M := by apply LinearMap.ext intro x apply PiLp.ext intro i simp [S, M, W, orthonormalColumnsLinearIsometry, Matrix.toEuclideanLin_apply, Matrix.mulVec_mulVec, ← Matrix.toEuclideanLin_conjTranspose_eq_adjoint] have hfactor (x : EuclideanSpace ℝ κ) : W (S x) = M x := by have hx : M x ∈ W.toLinearMap.range := by change V.toEuclideanLin x ∈ U.toEuclideanLin.range rw [hspace] exact LinearMap.mem_range_self V.toEuclideanLin x rcases hx with ⟨z, hz⟩ rw [hS, LinearMap.comp_apply, ← hz] have hleft := W.adjoint_comp_self have hleft_apply := congrArg (fun f => f z) hleft change W (W.toLinearMap.adjoint (W z)) = W z congr 1 have hgram : S.adjoint ∘ₗ S = M.adjoint ∘ₗ M := by apply LinearMap.ext intro x apply ext_inner_right ℝ intro y rw [LinearMap.comp_apply, LinearMap.comp_apply, S.adjoint_inner_left, M.adjoint_inner_left] rw [← W.inner_map_map (S x) (S y), hfactor x, hfactor y] have hsv : S.singularValues = M.singularValues := by simp only [singularValues, hgram] change S.singularValues (card κ - 1) = M.singularValues (card κ - 1) exact DFunLike.congr_fun hsv (card κ - 1) -
squareOperatorNorm_compress_letheorem — An orthonormal compression cannot increase the Euclidean operator norm of a square matrix. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionsquareOperatorNorm (U.transpose * A * U) ≤ squareOperatorNorm AProof (Lean source)
-- Proof route: interpret the product as the composition `U† ∘ A ∘ U`. Derive -- `‖U x‖ = ‖x‖` directly from `UᵀU = I`; use it for `‖U‖ ≤ 1`, and use Cauchy--Schwarz -- plus the same identity for the restricted adjoint estimate needed by the compression. theorem squareOperatorNorm_compress_le {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (U : Matrix ι κ ℝ) (A : Matrix ι ι ℝ) (horth : OrthonormalColumns U) : squareOperatorNorm (U.transpose * A * U) ≤ squareOperatorNorm A := by open scoped Matrix.Norms.L2Operator in change ‖U.transpose * A * U‖ ≤ ‖A‖ have hU := orthonormalColumns_l2OpNorm_le_one U horth have hUt : ‖U.transpose‖ ≤ 1 := by rw [show U.transpose = U.conjTranspose by ext i j; simp, Matrix.l2_opNorm_conjTranspose] exact hU calc ‖U.transpose * A * U‖ ≤ ‖U.transpose * A‖ * ‖U‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖U.transpose‖ * ‖A‖) * ‖U‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ ≤ (1 * ‖A‖) * 1 := by gcongr _ = ‖A‖ := by ring -
injective_of_pos_le_leastColumnSingularValuetheorem — A positive lower bound for the last column singular value implies full column rank. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionInjective A.toEuclideanLinProof (Lean source)
-- Proof route: positivity rules out -- `singularValues_eq_zero_iff_le_finrank_range` at the last domain index. Hence the range has -- full domain finrank, so rank--nullity makes the kernel trivial. (The existing expansion lemma -- itself assumes injectivity, so it cannot be used contrapositively here.) theorem injective_of_pos_le_leastColumnSingularValue {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq κ] [Nonempty κ] (A : Matrix ι κ ℝ) {sigma : ℝ} (hsigma : 0 < sigma) (hsv : sigma ≤ leastColumnSingularValue A) : Injective A.toEuclideanLin := by let T := A.toEuclideanLin have hpos : 0 < T.singularValues (card κ - 1) := lt_of_lt_of_le hsigma hsv have hrank_not : ¬ finrank ℝ T.range ≤ card κ - 1 := by intro hrank have hz := T.singularValues_eq_zero_iff_le_finrank_range.mpr hrank rw [hz] at hpos exact lt_irrefl 0 hpos have hcard_le : card κ ≤ finrank ℝ T.range := by omega have hrank_le : finrank ℝ T.range ≤ card κ := by simpa [T, finrank_euclideanSpace] using T.finrank_range_le have hker : finrank ℝ T.ker = 0 := by have hrank_null : finrank ℝ T.range + finrank ℝ T.ker = card κ := by simpa [finrank_euclideanSpace] using T.finrank_range_add_finrank_ker omega rw [← LinearMap.ker_eq_bot] exact Submodule.finrank_eq_zero.mp hker -
compressedLift_leastSingularValuetheorem — If a lifted factor has least singular value at least sigma, then its coordinates in any orthonormal basis of its column space have the same lower singular-value bound. Under the listed assumptions, the stated conclusion follows.hypothesesp n d :ℕNeZero nC :FactorMatrix p nsigma :ℝhsigma :0 < sigmahlift :sigma ≤ leastColumnSingularValue (liftedDirections d C)horth :hspace :SameColumnSpace U (liftedDirections d C)conclusionsigma ≤ leastColumnSingularValue (U.transpose * liftedDirections d C)Proof (Lean source)
theorem compressedLift_leastSingularValue {p n d : ℕ} [NeZero n] (C : FactorMatrix p n) (U : Matrix (LiftIndex p d) (Fin n) ℝ) {sigma : ℝ} (hsigma : 0 < sigma) (hlift : sigma ≤ leastColumnSingularValue (liftedDirections d C)) (horth : OrthonormalColumns U) (hspace : SameColumnSpace U (liftedDirections d C)) : sigma ≤ leastColumnSingularValue (U.transpose * liftedDirections d C) := by have hinj := injective_of_pos_le_leastColumnSingularValue (liftedDirections d C) hsigma hlift rw [leastColumnSingularValue_transpose_mul_eq U (liftedDirections d C) horth hspace hinj] exact hlift -
compressedLift_operatorNorm_le_sqrttheorem — The square coordinate matrix of a degree lift with unit columns has operator norm at most the square root of the number of factor columns. Under the listed assumptions, the stated conclusion follows.hypothesesconclusionProof (Lean source)
theorem compressedLift_operatorNorm_le_sqrt {p n d : ℕ} (C : FactorMatrix p n) (U : Matrix (LiftIndex p d) (Fin n) ℝ) (hd : 0 < d) (horth : OrthonormalColumns U) (hunit : ∀ j, finiteFrobeniusNorm (C.col j) = 1) : squareOperatorNorm (U.transpose * liftedDirections d C) ≤ sqrt n := by open scoped Matrix.Norms.L2Operator in change ‖U.transpose * liftedDirections d C‖ ≤ sqrt n have hU := orthonormalColumns_l2OpNorm_le_one U horth have hUt : ‖U.transpose‖ ≤ 1 := by rw [show U.transpose = U.conjTranspose by ext i j; simp, Matrix.l2_opNorm_conjTranspose] exact hU have hV : ‖liftedDirections d C‖ ≤ sqrt n := (rectangularOperatorNorm_le_matrixFrobenius (liftedDirections d C)).trans_eq (matrixFrobeniusNorm_liftedDirections hd C hunit) calc ‖U.transpose * liftedDirections d C‖ ≤ ‖U.transpose‖ * ‖liftedDirections d C‖ := Matrix.l2_opNorm_mul _ _ _ ≤ 1 * sqrt n := mul_le_mul hUt hV (norm_nonneg _) zero_le_one _ = sqrt n := one_mul _ -
compressedLift_inverse_operatorNorm_letheorem — The inverse of the square coordinate matrix of a well-conditioned degree lift has operator norm at most the reciprocal of the lifted least-singular-value margin. Under the listed assumptions, the stated conclusion follows.hypothesesp n d :ℕNeZero nC :FactorMatrix p nsigma :ℝhsigma :0 < sigmahlift :sigma ≤ leastColumnSingularValue (liftedDirections d C)horth :hspace :SameColumnSpace U (liftedDirections d C)conclusionsquareOperatorNorm (U.transpose * liftedDirections d C)⁻¹ ≤ sigma⁻¹Proof (Lean source)
theorem compressedLift_inverse_operatorNorm_le {p n d : ℕ} [NeZero n] (C : FactorMatrix p n) (U : Matrix (LiftIndex p d) (Fin n) ℝ) {sigma : ℝ} (hsigma : 0 < sigma) (hlift : sigma ≤ leastColumnSingularValue (liftedDirections d C)) (horth : OrthonormalColumns U) (hspace : SameColumnSpace U (liftedDirections d C)) : squareOperatorNorm (U.transpose * liftedDirections d C)⁻¹ ≤ sigma⁻¹ := by apply squareInverse_operatorNorm_le_reciprocal _ hsigma exact compressedLift_leastSingularValue C U hsigma hlift horth hspace -
compressedLift_condition_letheorem — A degree lift with unit columns and least singular value at least sigma has compressed diagonalizer condition number at most sqrt n / sigma. Under the listed assumptions, the stated conclusion follows.hypothesesp n d :ℕNeZero nC :FactorMatrix p nsigma :ℝhd :0 < dhsigma :0 < sigmahunit :∀ j, finiteFrobeniusNorm (C.col j) = 1hlift :sigma ≤ leastColumnSingularValue (liftedDirections d C)horth :hspace :SameColumnSpace U (liftedDirections d C)conclusionsquareOperatorNorm (U.transpose * liftedDirections d C) * squareOperatorNorm (U.transpose * liftedDirections d C)⁻¹≤ sqrt n / sigmaProof (Lean source)
theorem compressedLift_condition_le {p n d : ℕ} [NeZero n] (C : FactorMatrix p n) (U : Matrix (LiftIndex p d) (Fin n) ℝ) {sigma : ℝ} (hd : 0 < d) (hsigma : 0 < sigma) (hunit : ∀ j, finiteFrobeniusNorm (C.col j) = 1) (hlift : sigma ≤ leastColumnSingularValue (liftedDirections d C)) (horth : OrthonormalColumns U) (hspace : SameColumnSpace U (liftedDirections d C)) : squareOperatorNorm (U.transpose * liftedDirections d C) * squareOperatorNorm (U.transpose * liftedDirections d C)⁻¹ ≤ sqrt n / sigma := by have hop := compressedLift_operatorNorm_le_sqrt C U hd horth hunit have hinv := compressedLift_inverse_operatorNorm_le C U hsigma hlift horth hspace calc squareOperatorNorm (U.transpose * liftedDirections d C) * squareOperatorNorm (U.transpose * liftedDirections d C)⁻¹ ≤ sqrt n * sigma⁻¹ := mul_le_mul hop hinv (norm_nonneg _) (Real.sqrt_nonneg _) _ = sqrt n / sigma := by rw [div_eq_mul_inv] -
compressedNumerator_operatorNorm_letheorem — Every compressed numerator contraction has operator norm at most n * Lambda when the factor columns and the contraction probe are unit and the coefficients are bounded by Lambda. Under the listed assumptions, the stated conclusion follows.hypothesesp n d q :ℕC :FactorMatrix p nlam :Fin n → ℝu w :Vec pLambda :ℝhd :0 < dhq :0 < qhLambda :0 ≤ Lambdahorth :hunitC :∀ j, finiteFrobeniusNorm (C.col j) = 1hu :finiteFrobeniusNorm u = 1hw :finiteFrobeniusNorm w = 1hlam :∀ j, |lam j| ≤ LambdaconclusionsquareOperatorNorm (U.transpose * contractLast (decompositionTensor (d + d + q) C lam) (pencilProbes u w) * U)≤ n * LambdaProof (Lean source)
-- Proof route: use the exact contraction factorization, Cauchy--Schwarz for both loadings, -- `‖S‖ ≤ ‖S‖F = sqrt n`, and submultiplicativity. theorem compressedNumerator_operatorNorm_le {p n d q : ℕ} (C : FactorMatrix p n) (lam : Fin n → ℝ) (u w : Vec p) (U : Matrix (LiftIndex p d) (Fin n) ℝ) {Lambda : ℝ} (hd : 0 < d) (hq : 0 < q) (hLambda : 0 ≤ Lambda) (horth : OrthonormalColumns U) (hunitC : ∀ j, finiteFrobeniusNorm (C.col j) = 1) (hu : finiteFrobeniusNorm u = 1) (hw : finiteFrobeniusNorm w = 1) (hlam : ∀ j, |lam j| ≤ Lambda) : squareOperatorNorm (U.transpose * contractLast (decompositionTensor (d + d + q) C lam) (pencilProbes u w) * U) ≤ n * Lambda := by by_cases hn : n = 0 · subst n simp [squareOperatorNorm] letI : Nonempty (Fin n) := ⟨⟨0, Nat.pos_of_ne_zero hn⟩⟩ have hdot (x y : Vec p) (hx : finiteFrobeniusNorm x = 1) (hy : finiteFrobeniusNorm y = 1) : |dot x y| ≤ 1 := by have hsx : ∑ i, x i ^ 2 = 1 := by have h := congrArg (fun z : ℝ => z ^ 2) hx simpa [finiteFrobeniusNorm, Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] using h have hsy : ∑ i, y i ^ 2 = 1 := by have h := congrArg (fun z : ℝ => z ^ 2) hy simpa [finiteFrobeniusNorm, Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] using h have hcs := Finset.sum_mul_sq_le_sq_mul_sq (Finset.univ : Finset (Fin p)) x y rw [hsx, hsy, mul_one] at hcs apply (sq_le_sq₀ (abs_nonneg _) zero_le_one).mp simpa [dot, sq_abs] using hcs have hload (j : Fin n) : |lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j)| ≤ Lambda := by have huj := hdot u (C.col j) hu (hunitC j) have hwj := hdot w (C.col j) hw (hunitC j) rw [abs_mul, abs_mul, abs_pow] calc |lam j| * |dot u (C.col j)| ^ (q - 1) * |dot w (C.col j)| ≤ Lambda * 1 ^ (q - 1) * 1 := by gcongr exact hlam j _ = Lambda := by ring let S := U.transpose * liftedDirections d C let D := diagonal (fun j => lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j)) have hS : squareOperatorNorm S ≤ Real.sqrt n := compressedLift_operatorNorm_le_sqrt C U hd horth hunitC open scoped Matrix.Norms.L2Operator in change ‖S‖ ≤ Real.sqrt n at hS have hD : ‖D‖ ≤ Lambda := by change ‖Matrix.diagonal (fun j => lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j))‖ ≤ Lambda rw [Matrix.l2_opNorm_diagonal] apply (pi_norm_le_iff_of_nonempty _).2 intro j simpa [Real.norm_eq_abs] using hload j have hSt : ‖S.transpose‖ ≤ Real.sqrt n := by rw [show S.transpose = S.conjTranspose by ext i j; simp, Matrix.l2_opNorm_conjTranspose] exact hS rw [contractLast_decompositionTensor hq] change ‖U.transpose * (liftedDirections d C * D * (liftedDirections d C).transpose) * U‖ ≤ n * Lambda rw [show U.transpose * (liftedDirections d C * D * (liftedDirections d C).transpose) * U = S * D * S.transpose by simp [S, Matrix.transpose_mul, Matrix.mul_assoc]] have hn0 : (0 : ℝ) ≤ n := by positivity calc ‖S * D * S.transpose‖ ≤ ‖S * D‖ * ‖S.transpose‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖S‖ * ‖D‖) * ‖S.transpose‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ ≤ (Real.sqrt n * Lambda) * Real.sqrt n := by gcongr _ = n * Lambda := by rw [mul_assoc, mul_comm Lambda, ← mul_assoc, Real.mul_self_sqrt hn0]
Main 6 core · 1 supporting This module assembles contraction, lifted conditioning, pencil perturbation, spectral-projector matching, trace-coordinate recovery, and normalization into a permutation-aligned local inverse for finite symmetric rank-on ★ exists_permutation_factorMatrix_frobeniusNorm_le
Quantitative local inverse for symmetric tensor pencils
This module assembles contraction, lifted conditioning, pencil perturbation, spectral-projector matching, trace-coordinate recovery, and normalization into a permutation-aligned local inverse for finite symmetric rank-one tensor decompositions.
def contractedMargin reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The contracted denominator singular-value margin assembled from coefficient, probe, and lifted-factor margins. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
q :
ℕ
sigma kappa :
ℝ
def
contractedMargin q sigma kappa :
ℝ
given by
kappa * sigma ^ (q + 2)
def liftedConditionEnvelope reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The condition-number envelope for a lifted matrix with n unit columns and least singular value at least sigma, namely the square root of n divided by sigma. The formula is unguarded: it is a condition-number envelope only for positive sigma, and a zero margin gives zero by the division-by-zero convention. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
def localInverseRadius reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The admissible tensor perturbation radius for the quantitative tensor-pencil inverse. The formula is unguarded: it is an admissible radius only in the positive-margin regime assumed by the inverse theorem, and degenerate margins give zero by the division-by-zero convention. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
n q :
ℕ
sigma kappa Lambda :
ℝ
def
localInverseRadius n q sigma kappa Lambda :
ℝ
given by
eta :
contractedMargin q sigma kappa
chi :
liftedConditionEnvelope n sigma
h :
pencilPerturbationConstant n eta Lambda
min (eta / 2) (sigma / (6 * chi * h))
def traceRecoveryConstant reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The coordinatewise trace-recovery Lipschitz factor for the quantitative tensor-pencil inverse. The formula is unguarded: it is a valid Lipschitz factor only in the positive-margin regime assumed by the recovery theorems, and degenerate margins give zero by the division-by-zero convention. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
n q :
ℕ
sigma kappa Lambda :
ℝ
def
traceRecoveryConstant n q sigma kappa Lambda :
ℝ
given by
eta :
contractedMargin q sigma kappa
chi :
liftedConditionEnvelope n sigma
h :
pencilPerturbationConstant n eta Lambda
n * h * (2 * chi + 6 * n * Lambda * chi ^ 2 / (eta * sigma))
def factorRecoveryConstant reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
The final factor-matrix Frobenius Lipschitz factor for the quantitative tensor-pencil inverse. It is a fixed multiple of the trace-recovery factor and inherits its unguarded conventions: it is a valid Lipschitz factor only in the positive-margin regime of the recovery theorems. With its explicit inputs, the defined object is given by the displayed formula.
Definition (Lean source)
parameters
p n q :
ℕ
sigma kappa Lambda :
ℝ
def
factorRecoveryConstant p n q sigma kappa Lambda :
ℝ
given by
2 * sqrt (n * p) * traceRecoveryConstant n q sigma kappa Lambda
theorem exists_permutation_factorMatrix_frobeniusNorm_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Quantitative symmetric-tensor-pencil local inverse. Given two finite factor matrices, their coefficient vectors, two probes, the gap and coefficient margins, positive ambient dimensions and degrees, an admissible singular-value margin, positive and compatible coefficient bounds, unit probes, unit factor columns, two-sided coefficient bounds, positive denominator loadings, well-conditioned lifted directions, separated pencil ratios, and a tensor perturbation below the explicit local radius, one column permutation makes the factor-matrix Frobenius error at most the stated Lipschitz factor times the tensor Frobenius error. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
p n d q :
ℕ
C C' :
FactorMatrix p n
lam lam' :
Fin n → ℝ
u v :
Vec p
sigma kappa Lambda :
ℝ
hp :
0 < p
hn :
0 < n
hd :
0 < d
hq :
0 < q
hsigma :
0 < sigma ∧ sigma ≤ 1
hkappa :
0 < kappa
hkappaLambda :
kappa ≤ Lambda
hu :
finiteFrobeniusNorm u = 1
hv :
finiteFrobeniusNorm v = 1
hunit :
(∀ j, finiteFrobeniusNorm (C.col j) = 1) ∧ ∀ j, finiteFrobeniusNorm (C'.col j) = 1
hlam :
(∀ j, kappa ≤ |lam j| ∧ |lam j| ≤ Lambda) ∧ ∀ j, kappa ≤ |lam' j| ∧ |lam' j| ≤ Lambda
hprobe :
(∀ j, sigma ≤ dot u (C.col j)) ∧ ∀ j, sigma ≤ dot u (C'.col j)
hlift :
sigma ≤ leastColumnSingularValue (liftedDirections d C) ∧
sigma ≤ leastColumnSingularValue (liftedDirections d C')
hgap :
PairwiseGap (fun j => dot v (C.col j) / dot u (C.col j)) sigma ∧
PairwiseGap (fun j => dot v (C'.col j) / dot u (C'.col j)) sigma
hclose :
finiteFrobeniusNorm (decompositionTensor (d + d + q) C' lam' - decompositionTensor (d + d + q) C lam) < localInverseRadius n q sigma kappa Lambda
conclusion
matrixFrobeniusNorm (permuteColumns C' pi - C)
≤ factorRecoveryConstant p n q sigma kappa Lambda * finiteFrobeniusNorm (decompositionTensor (d + d + q) C' lam' - decompositionTensor (d + d + q) C lam)
Proof (Lean source)
-- Proof route: contract and compress using one orthonormal basis for the unprimed lifted range;
-- the denominator margin is `eta`, every coordinate pencil moves by at most `h*e`, and the
-- Riesz-projector theorem supplies one common permutation. Trace coordinates then move by
-- `Lz*e`; positive probe orientation makes their normalization equal the original columns.
--
-- A convenient detailed assembly is as follows.
-- 1. Put `V = liftedDirections d C`, choose an orthonormal basis of `V.toEuclideanLin.range`
-- (use `stdOrthonormalBasis` on the range subtype and reindex using the finrank equality from
-- injectivity), and write its ambient coordinate columns as `U`. Prove `OrthonormalColumns U`
-- and `SameColumnSpace U V`; put `S = U.transpose * V` and similarly `S'` for `C'`.
-- 2. Compress the `u` denominator contractions and coordinate numerator contractions by `U`.
-- The exact contraction identity identifies them with `S * diagonal * S.transpose` (and the
-- primed analogue). Contraction plus `squareOperatorNorm_compress_le` bounds every difference
-- by the tensor error `e`. The denominator theorem gives least singular value `eta`; inverse
-- perturbation makes the primed denominator invertible, and determinant multiplicativity then
-- makes `S'` invertible.
-- 3. Define the right pencils `G w` and `G' w`. `rightPencil_eq_diagonalization` identifies them
-- with the loading-ratio diagonalizations. For every standard basis probe,
-- `rightPencil_perturbation_bound` gives error `h*e`; the unprimed pencil norm is at most
-- `n*Lambda/eta` by numerator and inverse bounds.
-- 4. From `e < min (eta/2) (sigma/(6*chi*h))`, derive both smallness inequalities and apply
-- `exists_permutation_projector_matching` once. Feed that common permutation and its
-- projector bounds into `traceCoordinates_perturbation_bound`; after
-- `finiteFrobeniusNorm_sub_le_sqrt_mul`, each trace vector has error at most
-- `sqrt p * traceRecoveryConstant ... * e`.
-- 5. Exact trace diagonalization says those vectors are the positively rescaled columns.
-- Cauchy--Schwarz and the unit hypotheses make their norms at least one. Apply
-- `normalizeVec_sub_normalizeVec_le`, rewrite both normalizations with
-- `normalizeVec_inv_smul_eq`, and combine the column estimates using
-- `matrixFrobeniusNorm_le_sqrt_mul_of_columns`. Finish with
-- `Real.sqrt_mul` on the nonnegative natural casts and the definition of
-- `factorRecoveryConstant`.
theorem exists_permutation_factorMatrix_frobeniusNorm_le
{p n d q : ℕ} (C C' : FactorMatrix p n) (lam lam' : Fin n → ℝ)
(u v : Vec p) (sigma kappa Lambda : ℝ)
(hp : 0 < p) (hn : 0 < n) (hd : 0 < d) (hq : 0 < q)
(hsigma : 0 < sigma ∧ sigma ≤ 1) (hkappa : 0 < kappa)
(hkappaLambda : kappa ≤ Lambda)
(hu : finiteFrobeniusNorm u = 1) (hv : finiteFrobeniusNorm v = 1)
(hunit : (∀ j, finiteFrobeniusNorm (C.col j) = 1) ∧
∀ j, finiteFrobeniusNorm (C'.col j) = 1)
(hlam : (∀ j, kappa ≤ |lam j| ∧ |lam j| ≤ Lambda) ∧
∀ j, kappa ≤ |lam' j| ∧ |lam' j| ≤ Lambda)
(hprobe : (∀ j, sigma ≤ dot u (C.col j)) ∧
∀ j, sigma ≤ dot u (C'.col j))
(hlift : sigma ≤ leastColumnSingularValue (liftedDirections d C) ∧
sigma ≤ leastColumnSingularValue (liftedDirections d C'))
(hgap : PairwiseGap (fun j => dot v (C.col j) / dot u (C.col j)) sigma ∧
PairwiseGap (fun j => dot v (C'.col j) / dot u (C'.col j)) sigma)
(hclose : finiteFrobeniusNorm
(decompositionTensor (d + d + q) C' lam' -
decompositionTensor (d + d + q) C lam) <
localInverseRadius n q sigma kappa Lambda) :
∃ pi : Perm (Fin n),
matrixFrobeniusNorm (permuteColumns C' pi - C) ≤
factorRecoveryConstant p n q sigma kappa Lambda *
finiteFrobeniusNorm
(decompositionTensor (d + d + q) C' lam' -
decompositionTensor (d + d + q) C lam) := by
classical
letI : NeZero n := ⟨Nat.ne_of_gt hn⟩
let T := decompositionTensor (d + d + q) C lam
let T' := decompositionTensor (d + d + q) C' lam'
let e := finiteFrobeniusNorm (T' - T)
let eta := contractedMargin q sigma kappa
let chi := liftedConditionEnvelope n sigma
let h := pencilPerturbationConstant n eta Lambda
let Lz := traceRecoveryConstant n q sigma kappa Lambda
have hLambda : 0 < Lambda := lt_of_lt_of_le hkappa hkappaLambda
obtain ⟨heta, hchi, hh, hradius, hLz, _hfactor⟩ :=
localInverse_constants_pos hp hn hq hsigma.1 hkappa hkappaLambda
change 0 < eta at heta
change 0 < chi at hchi
change 0 < h at hh
change 0 < Lz at hLz
have he : 0 ≤ e := Real.sqrt_nonneg _
have heRadius : e < localInverseRadius n q sigma kappa Lambda := hclose
have heSmall : e < eta / 2 := by
exact heRadius.trans_le (min_le_left _ _)
have heProjector : 6 * chi * (h * e) < sigma := by
have heSecond : e < sigma / (6 * chi * h) :=
heRadius.trans_le (min_le_right _ _)
have hden : 0 < 6 * chi * h := mul_pos (mul_pos (by norm_num) hchi) hh
apply (lt_div_iff₀ hden).mp at heSecond
nlinarith
let V := liftedDirections d C
let V' := liftedDirections d C'
have hinjV : Injective V.toEuclideanLin :=
injective_of_pos_le_leastColumnSingularValue V hsigma.1 hlift.1
obtain ⟨U, hUorth, hUspace⟩ :=
exists_orthonormalColumns_sameColumnSpace V hinjV
let S := U.transpose * V
let S' := U.transpose * V'
let Au := U.transpose * contractLast T (pencilProbes u u) * U
let Au' := U.transpose * contractLast T' (pencilProbes u u) * U
let Aw : Vec p → Matrix (Fin n) (Fin n) ℝ := fun w =>
U.transpose * contractLast T (pencilProbes u w) * U
let Aw' : Vec p → Matrix (Fin n) (Fin n) ℝ := fun w =>
U.transpose * contractLast T' (pencilProbes u w) * U
have hpencilProbes (w : Vec p) (hw : finiteFrobeniusNorm w = 1) :
∀ a : Fin q, finiteFrobeniusNorm (pencilProbes u w a) ≤ 1 := by
intro a
simp only [pencilProbes]
split <;> simp_all
have hcompressedPert (w : Vec p) (hw : finiteFrobeniusNorm w = 1) :
squareOperatorNorm (Aw' w - Aw w) ≤ e := by
have hcontract : contractLast T' (pencilProbes u w) -
contractLast T (pencilProbes u w) =
contractLast (T' - T) (pencilProbes u w) := by
ext i j
simp only [contractLast, Matrix.sub_apply, Pi.sub_apply]
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro K _
ring
have hmatrix : Aw' w - Aw w =
U.transpose * contractLast (T' - T) (pencilProbes u w) * U := by
dsimp only [Aw, Aw']
rw [← Matrix.sub_mul, ← Matrix.mul_sub, hcontract]
rw [hmatrix]
exact (squareOperatorNorm_compress_le U
(contractLast (T' - T) (pencilProbes u w)) hUorth).trans
(contractLast_operatorNorm_le (T' - T) (pencilProbes u w)
(hpencilProbes w hw))
have hAuPert : squareOperatorNorm (Au' - Au) ≤ e := by
simpa only [Au, Au', Aw, Aw'] using hcompressedPert u hu
have hAuFactor : Au = S * diagonal
(fun j => lam j * dot u (C.col j) ^ q) * S.transpose := by
dsimp only [Au, T]
rw [contractLast_decompositionTensor hq]
have hdiag : diagonal (fun j =>
lam j * dot u (C.col j) ^ (q - 1) * dot u (C.col j)) =
diagonal (fun j => lam j * dot u (C.col j) ^ q) := by
congr 1
funext j
rw [mul_assoc, pow_sub_one_mul (Nat.ne_of_gt hq)]
rw [hdiag]
simp only [S, V, Matrix.transpose_mul, Matrix.transpose_transpose, Matrix.mul_assoc]
have hAuFactor' : Au' = S' * diagonal
(fun j => lam' j * dot u (C'.col j) ^ q) * S'.transpose := by
dsimp only [Au', T']
rw [contractLast_decompositionTensor hq]
have hdiag : diagonal (fun j =>
lam' j * dot u (C'.col j) ^ (q - 1) * dot u (C'.col j)) =
diagonal (fun j => lam' j * dot u (C'.col j) ^ q) := by
congr 1
funext j
rw [mul_assoc, pow_sub_one_mul (Nat.ne_of_gt hq)]
rw [hdiag]
simp only [S', V', Matrix.transpose_mul, Matrix.transpose_transpose, Matrix.mul_assoc]
have hAuSv : eta ≤ leastColumnSingularValue Au := by
rw [hAuFactor]
exact compressedDenominator_leastSingularValue C lam u U hq hsigma.1 hkappa
hUorth hUspace hlift.1 (fun j => hlam.1 j |>.1) hprobe.1
obtain ⟨hAuUnit, hAuInv⟩ := inverse_operatorNorm_le_reciprocal Au heta hAuSv
obtain ⟨hAuUnit', hAuInv', hAuInvPert⟩ :=
inverse_perturbation_bound Au Au' heta he hAuSv hAuPert heSmall
have hSsv : sigma ≤ leastColumnSingularValue S :=
compressedLift_leastSingularValue C U hsigma.1 hlift.1 hUorth hUspace
obtain ⟨hS, _hSinv⟩ := inverse_operatorNorm_le_reciprocal S hsigma.1 hSsv
have hS' : IsUnit S'.det := by
apply isUnit_iff_ne_zero.mpr
intro hzero
have hdetzero : Au'.det = 0 := by
rw [hAuFactor', Matrix.det_mul, Matrix.det_mul, hzero]
simp
exact (isUnit_iff_ne_zero.mp hAuUnit') hdetzero
have hcondition : squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi := by
exact compressedLift_condition_le C U hd hsigma.1 hunit.1 hlift.1 hUorth hUspace
have hstandard (i : Fin p) : finiteFrobeniusNorm (standardBasis p i) = 1 := by
unfold finiteFrobeniusNorm standardBasis
simp
have hAwNorm (i : Fin p) : squareOperatorNorm (Aw (standardBasis p i)) ≤
n * Lambda := by
exact compressedNumerator_operatorNorm_le C lam u (standardBasis p i) U hd hq
hLambda.le hUorth hunit.1 hu (hstandard i) (fun j => hlam.1 j |>.2)
let G : Vec p → Matrix (Fin n) (Fin n) ℝ := fun w => rightPencil (Aw w) Au
let G' : Vec p → Matrix (Fin n) (Fin n) ℝ := fun w => rightPencil (Aw' w) Au'
let values : Fin n → ℝ := fun j => dot v (C.col j) / dot u (C.col j)
let values' : Fin n → ℝ := fun j => dot v (C'.col j) / dot u (C'.col j)
have hprobePos (j : Fin n) : 0 < dot u (C.col j) :=
hsigma.1.trans_le (hprobe.1 j)
have hprobePos' (j : Fin n) : 0 < dot u (C'.col j) :=
hsigma.1.trans_le (hprobe.2 j)
have hload (j : Fin n) : lam j * dot u (C.col j) ^ q ≠ 0 :=
mul_ne_zero (abs_pos.mp (lt_of_lt_of_le hkappa (hlam.1 j).1))
(pow_ne_zero _ (hprobePos j).ne')
have hload' (j : Fin n) : lam' j * dot u (C'.col j) ^ q ≠ 0 :=
mul_ne_zero (abs_pos.mp (lt_of_lt_of_le hkappa (hlam.2 j).1))
(pow_ne_zero _ (hprobePos' j).ne')
have hAwFactor (w : Vec p) : Aw w = S * diagonal (fun j =>
lam j * (dot u (C.col j) ^ (q - 1) * dot w (C.col j))) * S.transpose := by
dsimp only [Aw, T]
rw [contractLast_decompositionTensor hq]
have hdiag : diagonal (fun j =>
lam j * dot u (C.col j) ^ (q - 1) * dot w (C.col j)) =
diagonal (fun j =>
lam j * (dot u (C.col j) ^ (q - 1) * dot w (C.col j))) := by
congr 1
funext j
ring
rw [hdiag]
simp only [S, V, Matrix.transpose_mul, Matrix.transpose_transpose, Matrix.mul_assoc]
have hAwFactor' (w : Vec p) : Aw' w = S' * diagonal (fun j =>
lam' j * (dot u (C'.col j) ^ (q - 1) * dot w (C'.col j))) * S'.transpose := by
dsimp only [Aw', T']
rw [contractLast_decompositionTensor hq]
have hdiag : diagonal (fun j =>
lam' j * dot u (C'.col j) ^ (q - 1) * dot w (C'.col j)) =
diagonal (fun j =>
lam' j * (dot u (C'.col j) ^ (q - 1) * dot w (C'.col j))) := by
congr 1
funext j
ring
rw [hdiag]
simp only [S', V', Matrix.transpose_mul, Matrix.transpose_transpose, Matrix.mul_assoc]
have hGdiag (w : Vec p) : G w = diagonalizableMatrix S
(fun j => dot w (C.col j) / dot u (C.col j)) := by
dsimp only [G]
rw [hAwFactor, hAuFactor]
rw [rightPencil_eq_diagonalization S lam
(fun j => dot u (C.col j) ^ q)
(fun j => dot u (C.col j) ^ (q - 1) * dot w (C.col j)) hS hload]
have hratio : (fun j => dot u (C.col j) ^ (q - 1) * dot w (C.col j) /
dot u (C.col j) ^ q) =
(fun j => dot w (C.col j) / dot u (C.col j)) := by
funext j
field_simp [(hprobePos j).ne']
calc
_ = (dot u (C.col j) ^ (q - 1) * dot u (C.col j)) *
dot w (C.col j) := by ring
_ = dot u (C.col j) ^ q * dot w (C.col j) := by
rw [pow_sub_one_mul (Nat.ne_of_gt hq)]
_ = _ := by ring
rw [hratio]
rfl
have hGdiag' (w : Vec p) : G' w = diagonalizableMatrix S'
(fun j => dot w (C'.col j) / dot u (C'.col j)) := by
dsimp only [G']
rw [hAwFactor', hAuFactor']
rw [rightPencil_eq_diagonalization S' lam'
(fun j => dot u (C'.col j) ^ q)
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
localInverse_constants_postheorem — For positive dimensions and admissible positive margins, the contracted margin, lifted condition envelope, pencil constant, local radius, trace constant, and factor constant are all strictly positive. Under the listed assumptions, the stated conclusion follows.hypothesesp n q :ℕhp :0 < phn :0 < nhq :0 < qsigma kappa Lambda :ℝhsigma :0 < sigmahkappa :0 < kappahkappaLambda :kappa ≤ Lambdaconclusionconclusion 10 < contractedMargin q sigma kappaconclusion 20 < liftedConditionEnvelope n sigmaconclusion 30 < pencilPerturbationConstant n (contractedMargin q sigma kappa) Lambdaconclusion 40 < localInverseRadius n q sigma kappa Lambdaconclusion 50 < traceRecoveryConstant n q sigma kappa Lambdaconclusion 60 < factorRecoveryConstant p n q sigma kappa LambdaProof (Lean source)
-- Proof route: unfold the six constants in dependency order. `Real.sqrt_pos.2` handles the -- two dimension square roots; `pow_pos`, division positivity, and `min_pos` handle the remaining -- arithmetic. Derive `0 < Lambda` from `hkappa` and `hkappaLambda` before proving positivity of -- `pencilPerturbationConstant`. theorem localInverse_constants_pos {p n q : ℕ} (hp : 0 < p) (hn : 0 < n) (hq : 0 < q) {sigma kappa Lambda : ℝ} (hsigma : 0 < sigma) (hkappa : 0 < kappa) (hkappaLambda : kappa ≤ Lambda) : 0 < contractedMargin q sigma kappa ∧ 0 < liftedConditionEnvelope n sigma ∧ 0 < pencilPerturbationConstant n (contractedMargin q sigma kappa) Lambda ∧ 0 < localInverseRadius n q sigma kappa Lambda ∧ 0 < traceRecoveryConstant n q sigma kappa Lambda ∧ 0 < factorRecoveryConstant p n q sigma kappa Lambda := by have hLambda : 0 < Lambda := lt_of_lt_of_le hkappa hkappaLambda have heta : 0 < contractedMargin q sigma kappa := by unfold contractedMargin exact mul_pos hkappa (pow_pos hsigma _) have hsqrtn : 0 < sqrt n := Real.sqrt_pos.2 (Nat.cast_pos.2 hn) have hchi : 0 < liftedConditionEnvelope n sigma := by unfold liftedConditionEnvelope exact div_pos hsqrtn hsigma have hh : 0 < pencilPerturbationConstant n (contractedMargin q sigma kappa) Lambda := by unfold pencilPerturbationConstant positivity have hradius : 0 < localInverseRadius n q sigma kappa Lambda := by unfold localInverseRadius exact lt_min (div_pos heta (by norm_num)) (div_pos hsigma (mul_pos (mul_pos (by norm_num) hchi) hh)) have htrace : 0 < traceRecoveryConstant n q sigma kappa Lambda := by unfold traceRecoveryConstant positivity have hfactor : 0 < factorRecoveryConstant p n q sigma kappa Lambda := by unfold factorRecoveryConstant have hsqrtnp : 0 < sqrt (n * p) := Real.sqrt_pos.2 (mul_pos (Nat.cast_pos.2 hn) (Nat.cast_pos.2 hp)) positivity exact ⟨heta, hchi, hh, hradius, htrace, hfactor⟩
Projectors 1 core · 2 supporting This module states a quantitative finite-dimensional matching theorem for two real matrices with simple, separated, real spectra. ★ exists_permutation_projector_matching
Gap-based matching of spectral projectors
This module states a quantitative finite-dimensional matching theorem for two real matrices with simple, separated, real spectra. Projectors are represented algebraically through the respective diagonalizers, while the proof route is the usual complex Riesz-contour argument. Mathlib's circle-integral Cauchy formulas supply the scalar residue calculation; the resolvent bounds themselves use the explicitly supplied reference diagonalizer and a Neumann argument.
theorem exists_permutation_projector_matching reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SymmetricTensorPencil
Given two diagonalizers, their simple spectra, invertibility, positive separation, conditioning, and error margins, separation of both spectra, a diagonalizer condition bound, a pencil perturbation bound, and the required small-error condition, one permutation matches the simple spectral projectors with explicit eigenvalue and operator-norm bounds. Under the listed assumptions, the stated conclusion follows.
Formal statement
hypotheses
n :
ℕ
NeZero n
values values' :
Fin n → ℝ
sigma chi delta :
ℝ
hS :
IsUnit S.det
hS' :
IsUnit S'.det
hsigma :
0 < sigma
hchi :
0 < chi
hdelta :
0 ≤ delta
hgap :
PairwiseGap values sigma
hgap' :
PairwiseGap values' sigma
hcondition :
squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi
hclose :
≤ delta
hsmall :
6 * chi * delta < sigma
conclusion
∀ j,
|values' (pi j) - values j| < sigma / 3 ∧
≤ 6 * chi ^ 2 * delta / sigma ∧
squareOperatorNorm (coordinateProjector S j) ≤ chi ∧
squareOperatorNorm (coordinateProjector S' (pi j)) ≤ 2 * chi
Proof (Lean source)
-- Proof route: apply `diagonalizableMatrix_eigenvalue_localization`, turn the resulting
-- one-sided localization into a permutation with `exists_permutation_matching_of_localization`,
-- and apply `coordinateProjector_perturbation_of_matched_eigenvalue` along that permutation.
theorem exists_permutation_projector_matching {n : ℕ} [NeZero n]
(S S' : Matrix (Fin n) (Fin n) ℝ) (values values' : Fin n → ℝ)
{sigma chi delta : ℝ}
(hS : IsUnit S.det) (hS' : IsUnit S'.det)
(hsigma : 0 < sigma) (hchi : 0 < chi) (hdelta : 0 ≤ delta)
(hgap : PairwiseGap values sigma) (hgap' : PairwiseGap values' sigma)
(hcondition : squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi)
(hclose : squareOperatorNorm
(diagonalizableMatrix S' values' - diagonalizableMatrix S values) ≤ delta)
(hsmall : 6 * chi * delta < sigma) :
∃ pi : Perm (Fin n), ∀ j,
|values' (pi j) - values j| < sigma / 3 ∧
squareOperatorNorm (coordinateProjector S' (pi j) - coordinateProjector S j) ≤
6 * chi ^ 2 * delta / sigma ∧
squareOperatorNorm (coordinateProjector S j) ≤ chi ∧
squareOperatorNorm (coordinateProjector S' (pi j)) ≤ 2 * chi := by
have hlocal := diagonalizableMatrix_eigenvalue_localization S S' values values'
hS hS' hcondition hclose
have hradius : 0 ≤ chi * delta := mul_nonneg hchi.le hdelta
have htwosmall : 2 * (chi * delta) < sigma := by linarith
obtain ⟨pi, hpi⟩ := exists_permutation_matching_of_localization values values'
hradius hgap' hlocal htwosmall
refine ⟨pi, fun j => ?_⟩
have hmatch := hpi j
have hthird : |values' (pi j) - values j| < sigma / 3 := by linarith
exact ⟨hthird,
coordinateProjector_perturbation_of_matched_eigenvalue S S' values values' j (pi j)
hS hS' hsigma hchi hdelta hgap hgap' hcondition hclose hmatch hsmall⟩
2 supporting declarations (lemmas, instances)
-
abs_trace_le_card_mul_operatorNormtheorem — The trace of a real square matrix is at most the dimension times its Euclidean operator norm in absolute value. The stated conclusion follows.Proof (Lean source)
theorem abs_trace_le_card_mul_operatorNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : |trace A| ≤ n * squareOperatorNorm A := by classical have hentry (i : Fin n) : |A i i| ≤ squareOperatorNorm A := by let e : EuclideanSpace ℝ (Fin n) := toLp 2 (single i 1) have he : ‖e‖ = 1 := by simp [e] have hcoord : |((EuclideanSpace.equiv (Fin n) ℝ).symm (mulVec A e)) i| ≤ ‖(EuclideanSpace.equiv (Fin n) ℝ).symm (mulVec A e)‖ := by simpa only [Real.norm_eq_abs] using PiLp.norm_apply_le ((EuclideanSpace.equiv (Fin n) ℝ).symm (mulVec A e)) i calc |A i i| = |((EuclideanSpace.equiv (Fin n) ℝ).symm (mulVec A e)) i| := by simp [e] _ ≤ ‖(EuclideanSpace.equiv (Fin n) ℝ).symm (mulVec A e)‖ := hcoord _ ≤ ‖A‖ * ‖e‖ := Matrix.l2_opNorm_mulVec A e _ = ‖A‖ := by rw [he, mul_one] _ = ‖(Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ)) A‖ := (Matrix.l2_opNorm_toEuclideanCLM A).symm _ = squareOperatorNorm A := rfl calc |trace A| = |∑ i, A i i| := rfl _ ≤ ∑ i, |A i i| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _ : Fin n, squareOperatorNorm A := Finset.sum_le_sum fun i _ => hentry i _ = n * squareOperatorNorm A := by simp -
coordinateProjector_perturbation_of_matched_eigenvaluetheorem — Matched simple eigenvalues of two nearby diagonalizable matrices have close coordinate projectors, and the perturbed projector remains controlled by twice the reference condition envelope. Under the listed assumptions, the stated conclusion follows.hypothesesn :ℕNeZero nvalues values' :Fin n → ℝj j' :Fin nsigma chi delta :ℝhS :IsUnit S.dethS' :IsUnit S'.dethsigma :0 < sigmahchi :0 < chihdelta :0 ≤ deltahgap :PairwiseGap values sigmahgap' :PairwiseGap values' sigmahcondition :squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chihclose :≤ deltahmatch :|values' j' - values j| ≤ chi * deltahsmall :6 * chi * delta < sigmaconclusionconclusion 1≤ 6 * chi ^ 2 * delta / sigmaconclusion 2squareOperatorNorm (coordinateProjector S j) ≤ chiconclusion 3squareOperatorNorm (coordinateProjector S' j') ≤ 2 * chiProof (Lean source)
-- Proof route: complexify and use the circle of radius `sigma / 3` about `values j`. -- Bauer--Fike localization and `hsmall` keep the Neumann resolvent along that circle invertible; -- the resolvent identity bounds the contour-integral difference. Algebraic identification of -- those Riesz integrals with the two coordinate projectors gives the three stated estimates. theorem coordinateProjector_perturbation_of_matched_eigenvalue {n : ℕ} [NeZero n] (S S' : Matrix (Fin n) (Fin n) ℝ) (values values' : Fin n → ℝ) (j j' : Fin n) {sigma chi delta : ℝ} (hS : IsUnit S.det) (hS' : IsUnit S'.det) (hsigma : 0 < sigma) (hchi : 0 < chi) (hdelta : 0 ≤ delta) (hgap : PairwiseGap values sigma) (hgap' : PairwiseGap values' sigma) (hcondition : squareOperatorNorm S * squareOperatorNorm S⁻¹ ≤ chi) (hclose : squareOperatorNorm (diagonalizableMatrix S' values' - diagonalizableMatrix S values) ≤ delta) (hmatch : |values' j' - values j| ≤ chi * delta) (hsmall : 6 * chi * delta < sigma) : squareOperatorNorm (coordinateProjector S' j' - coordinateProjector S j) ≤ 6 * chi ^ 2 * delta / sigma ∧ squareOperatorNorm (coordinateProjector S j) ≤ chi ∧ squareOperatorNorm (coordinateProjector S' j') ≤ 2 * chi := by let c : ℂ := (values j : ℂ) let R : ℝ := sigma / 3 let E := diagonalizableMatrix S' values' - diagonalizableMatrix S values have hR : 0 < R := by dsimp [R]; positivity have hchidelta : chi * delta < sigma / 6 := by linarith have hcircle_norm {z : ℂ} (hz : z ∈ sphere c R) : ‖z - c‖ = R := by rw [← dist_eq_norm] exact Metric.mem_sphere.mp hz have href_dist {z : ℂ} (hz : z ∈ sphere c R) : ∀ k, sigma / 3 ≤ ‖z - (values k : ℂ)‖ := by intro k by_cases hkj : k = j · subst k simpa [c, R] using (hcircle_norm hz).ge · have hgapkj : sigma ≤ ‖(values k : ℂ) - c‖ := by calc sigma ≤ |values k - values j| := by simpa [abs_sub_comm] using hgap k j hkj _ = ‖((values k - values j : ℝ) : ℂ)‖ := by rw [Complex.norm_real, Real.norm_eq_abs] _ = ‖(values k : ℂ) - (values j : ℂ)‖ := by norm_cast _ = ‖(values k : ℂ) - c‖ := by rw [show c = (values j : ℂ) by rfl] have htri := norm_sub_le_norm_sub_add_norm_sub (values k : ℂ) z c have hzc := hcircle_norm hz rw [norm_sub_rev (values k : ℂ) z] at htri dsimp [R] at hzc linarith have hprime_in : ‖(values' j' : ℂ) - c‖ < R := by have hm : ‖(values' j' : ℂ) - c‖ ≤ chi * delta := by calc _ = ‖((values' j' - values j : ℝ) : ℂ)‖ := by rw [show c = (values j : ℂ) by rfl] norm_cast _ = |values' j' - values j| := by rw [Complex.norm_real, Real.norm_eq_abs] _ ≤ _ := hmatch dsimp [R] linarith have hprime_out : ∀ k, k ≠ j' → R < ‖(values' k : ℂ) - c‖ := by intro k hkj' have hgapkj : sigma ≤ ‖(values' k : ℂ) - (values' j' : ℂ)‖ := by calc sigma ≤ |values' k - values' j'| := by simpa [abs_sub_comm] using hgap' k j' hkj' _ = ‖((values' k - values' j' : ℝ) : ℂ)‖ := by rw [Complex.norm_real, Real.norm_eq_abs] _ = _ := by norm_cast have htri := norm_sub_le_norm_sub_add_norm_sub (values' k : ℂ) c (values' j' : ℂ) have hm : ‖c - (values' j' : ℂ)‖ ≤ chi * delta := by rw [norm_sub_rev] calc _ = ‖((values' j' - values j : ℝ) : ℂ)‖ := by rw [show c = (values j : ℂ) by rfl] norm_cast _ = |values' j' - values j| := by rw [Complex.norm_real, Real.norm_eq_abs] _ ≤ _ := hmatch dsimp [R] linarith have href_out : ∀ k, k ≠ j → R < ‖(values k : ℂ) - c‖ := by intro k hkj have hg : sigma ≤ ‖(values k : ℂ) - c‖ := by calc sigma ≤ |values k - values j| := by simpa [abs_sub_comm] using hgap k j hkj _ = ‖((values k - values j : ℝ) : ℂ)‖ := by rw [Complex.norm_real, Real.norm_eq_abs] _ = ‖(values k : ℂ) - (values j : ℂ)‖ := by norm_cast _ = _ := by rw [show c = (values j : ℂ) by rfl] dsimp [R] linarith have href_ne {z : ℂ} (hz : z ∈ sphere c R) : ∀ k, z ≠ (values k : ℂ) := by intro k hzk subst z have := href_dist hz k simp only [sub_self, norm_zero] at this linarith have hprime_ne {z : ℂ} (hz : z ∈ sphere c R) : ∀ k, z ≠ (values' k : ℂ) := by intro k hzk subst z by_cases hkj : k = j' · subst k have heq := hcircle_norm hz linarith · have hout := hprime_out k hkj have heq := hcircle_norm hz linarith have hE : ‖complexMatrix E‖ ≤ delta := by rw [complexMatrix_norm_eq] simpa only [E, squareOperatorNorm, Matrix.l2_opNorm_toEuclideanCLM] using hclose let r : ℝ := 3 * chi / sigma have hrpos : 0 < r := by dsimp [r]; positivity have href_norm {z : ℂ} (hz : z ∈ sphere c R) : ‖complexResolvent S values z‖ ≤ r := by dsimp [r] exact complexResolvent_norm_le S values z hsigma hcondition (href_dist hz) have hdelta_r : delta * r < 1 / 2 := by dsimp [r] rw [show delta * (3 * chi / sigma) = (3 * chi * delta) / sigma by ring] apply (div_lt_iff₀ hsigma).2 nlinarith [hsmall] have hprime_norm {z : ℂ} (hz : z ∈ sphere c R) : ‖complexResolvent S' values' z‖ ≤ 2 * r := by have hid := complex_resolvent_identity S S' values values' z hS hS' (href_ne hz) (hprime_ne hz) have hdiff : ‖complexResolvent S' values' z - complexResolvent S values z‖ ≤ (‖complexResolvent S' values' z‖ * delta) * r := by rw [hid] calc ‖complexResolvent S' values' z * complexMatrix E * complexResolvent S values z‖ ≤ ‖complexResolvent S' values' z * complexMatrix E‖ * ‖complexResolvent S values z‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖complexResolvent S' values' z‖ * ‖complexMatrix E‖) * ‖complexResolvent S values z‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ ≤ (‖complexResolvent S' values' z‖ * delta) * ‖complexResolvent S values z‖ := by exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hE (norm_nonneg _)) (norm_nonneg _) _ ≤ (‖complexResolvent S' values' z‖ * delta) * r := by exact mul_le_mul_of_nonneg_left (href_norm hz) (mul_nonneg (norm_nonneg _) hdelta) have hsum : ‖complexResolvent S' values' z‖ ≤ ‖complexResolvent S' values' z - complexResolvent S values z‖ + ‖complexResolvent S values z‖ := by calc ‖complexResolvent S' values' z‖ = ‖(complexResolvent S' values' z - complexResolvent S values z) + complexResolvent S values z‖ := by congr 1; abel _ ≤ _ := norm_add_le _ _ nlinarith [href_norm hz, norm_nonneg (complexResolvent S' values' z)] have hint_bound {z : ℂ} (hz : z ∈ sphere c R) : ‖complexResolvent S' values' z - complexResolvent S values z‖ ≤ 18 * chi ^ 2 * delta / sigma ^ 2 := by rw [complex_resolvent_identity S S' values values' z hS hS' (href_ne hz) (hprime_ne hz)] calc ‖complexResolvent S' values' z * complexMatrix E * complexResolvent S values z‖ ≤ ‖complexResolvent S' values' z * complexMatrix E‖ * ‖complexResolvent S values z‖ := Matrix.l2_opNorm_mul _ _ _ ≤ (‖complexResolvent S' values' z‖ * ‖complexMatrix E‖) * ‖complexResolvent S values z‖ := by gcongr exact Matrix.l2_opNorm_mul _ _ _ ≤ (‖complexResolvent S' values' z‖ * delta) * ‖complexResolvent S values z‖ := by exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hE (norm_nonneg _)) (norm_nonneg _) _ ≤ ((2 * r) * delta) * ‖complexResolvent S values z‖ := by exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right (hprime_norm hz) hdelta) (norm_nonneg _) _ ≤ ((2 * r) * delta) * r := by exact mul_le_mul_of_nonneg_left (href_norm hz) (mul_nonneg (mul_nonneg (by positivity) hrpos.le) hdelta) _ = 18 * chi ^ 2 * delta / sigma ^ 2 := by dsimp [r] field_simp ring have hcontour : ‖(2 * pi * Complex.I : ℂ)⁻¹ • (∮ z in C(c, R), (complexResolvent S' values' z - complexResolvent S values z))‖ ≤ 6 * chi ^ 2 * delta / sigma := by calc _ ≤ R * (18 * chi ^ 2 * delta / sigma ^ 2) := circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le (fun z hz => hint_bound hz) _ = 6 * chi ^ 2 * delta / sigma := by dsimp [R] field_simp ring have href_int := complexResolvent_integral_eq_projector S values j c hR (by simp [c, R, hR]) href_out have hprime_int := complexResolvent_integral_eq_projector S' values' j' c hR hprime_in hprime_out have hintS : CircleIntegrable (fun z => complexResolvent S values z) c R := by apply complexResolvent_circleIntegrable S values c hR.le intro k hk exact href_ne hk k rfl have hintS' : CircleIntegrable (fun z => complexResolvent S' values' z) c R := by apply complexResolvent_circleIntegrable S' values' c hR.le intro k hk exact hprime_ne hk k rfl have hprojector_diff : complexMatrix (coordinateProjector S' j' - coordinateProjector S j) = (2 * pi * Complex.I : ℂ)⁻¹ • (∮ z in C(c, R), (complexResolvent S' values' z - complexResolvent S values z)) := by rw [complexMatrix_sub, circleIntegral.integral_sub hintS' hintS, smul_sub, hprime_int, href_int] have hdiff_real : squareOperatorNorm (coordinateProjector S' j' - coordinateProjector S j) ≤ 6 * chi ^ 2 * delta / sigma := by rw [squareOperatorNorm] rw [Matrix.l2_opNorm_toEuclideanCLM (coordinateProjector S' j' - coordinateProjector S j)] rw [← complexMatrix_norm_eq] rw [hprojector_diff] exact hcontour have hP := coordinateProjector_operatorNorm_le S j hS hcondition have hP' : squareOperatorNorm (coordinateProjector S' j') ≤ 2 * chi := by calc squareOperatorNorm (coordinateProjector S' j') = squareOperatorNorm ((coordinateProjector S' j' - coordinateProjector S j) + coordinateProjector S j) := by congr 2; abel _ ≤ squareOperatorNorm (coordinateProjector S' j' - coordinateProjector S j) + squareOperatorNorm (coordinateProjector S j) := by unfold squareOperatorNorm rw [map_add] exact norm_add_le _ _ _ ≤ 6 * chi ^ 2 * delta / sigma + chi := add_le_add hdiff_real hP _ ≤ 2 * chi := by have herr_lt : 6 * chi ^ 2 * delta / sigma < chi := by apply (div_lt_iff₀ hsigma).2 nlinarith [hsmall] linarith exact ⟨hdiff_real, hP, hP'⟩