Weyl's Inequality (1912)

For two m × n real matrices A, B with ordered singular values, the maximum pointwise difference between corresponding singular values is bounded by the operator norm of their difference.

def SVD.IsOrdered {d T : ℕ} (S : SVD d T) : Prop

An SVD decomposition with singular values in non-increasing order.

def SVD.HasTrueSingularValues {d T : ℕ} (S : SVD d T) (A : Matrix (Fin d) (Fin T) ℝ) : Prop

An SVD decomposition has "true" singular values if its σval matches Mathlib's canonical LinearMap.singularValues for the matrix it decomposes. This is needed because the SVD structure does not enforce orthonormality of singular vectors, so its σval may differ from the canonical singular values.

Operator norm symmetry

theorem matrixOpNorm_neg_sub {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) : matrixOpNorm (B - A) = matrixOpNorm (A - B)

Weyl bound for canonical singular values

The following axiom states the one-sided Weyl bound for Mathlib's canonical LinearMap.singularValues. This is a correct mathematical statement about the true singular values of a matrix.

The proof uses the Courant–Fischer minimax characterization of singular values (Bhatia "Matrix Analysis" Theorem III.1.2), which is not available in Mathlib. The textbook states Weyl's inequality without proof (Section 4.1, "Useful matrix inequalities"), citing Weyl (1912).

theorem weyl_singular_values_bound {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) (k : ℕ) : (Matrix.toEuclideanLin A).singularValues k ≤ (Matrix.toEuclideanLin B).singularValues k + matrixOpNorm (A - B)

Weyl's one-sided bound for canonical singular values (1912). For two m × n matrices A, B and any index k: σ_k(A) ≤ σ_k(B) + ‖A - B‖_op where σ_k denotes the k-th canonical singular value (via Mathlib's LinearMap.singularValues).

This is axiomatized because the textbook states it without proof (Section 4.1, "Useful matrix inequalities") and its standard proof requires the Courant–Fischer minimax theorem, which is not in Mathlib.

Note: This axiom is about Mathlib's canonical singular values, which are the correct mathematical objects. It would be unsound to state this for the custom SVD structure's σval without an orthonormality constraint.

One-sided Weyl bound for custom SVD

theorem weyl_one_sided {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) (S_A S_B : SVD d T) (hr : S_A.r = S_B.r) (hA_true : S_A.HasTrueSingularValues A) (hB_true : S_B.HasTrueSingularValues B) (k : Fin S_A.r) : S_A.σval k ≤ S_B.σval (Fin.cast hr k) + matrixOpNorm (A - B)

One-sided Weyl bound. For each k, σ_k(A) ≤ σ_k(B) + ‖A - B‖_op. This is derived from weyl_singular_values_bound (the axiom about canonical singular values) together with the HasTrueSingularValues hypothesis that connects the custom SVD's σval to the canonical values.

theorem weyl_inequality {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) (S_A S_B : SVD d T) (hr : S_A.r = S_B.r) (hA_true : S_A.HasTrueSingularValues A) (hB_true : S_B.HasTrueSingularValues B) (k : Fin S_A.r) : |S_A.σval k - S_B.σval (Fin.cast hr k)| ≤ matrixOpNorm (A - B)

Weyl's inequality (1912). For two m × n matrices A and B with SVD decompositions having the same number of components r and true singular values (matching Mathlib's canonical values):

|σ_k(A) - σ_k(B)| ≤ ‖A - B‖_op for each k

Proved from the one-sided bound weyl_one_sided applied in both directions.

theorem weyl_inequality_max {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) (S_A S_B : SVD d T) (hr : S_A.r = S_B.r) (hr_pos : 0 < S_A.r) (hA_true : S_A.HasTrueSingularValues A) (hB_true : S_B.HasTrueSingularValues B) : (Finset.univ.sup' ⋯ fun (k : Fin S_A.r) => ‖S_A.σval k - S_B.σval (Fin.cast hr k)‖₊) ≤ ‖matrixOpNorm (A - B)‖₊

Weyl's inequality (max form). The maximum over all k of the pointwise singular value differences is bounded by the operator norm:

max_k |σ_k(A) - σ_k(B)| ≤ ‖A - B‖_op

Derived from the pointwise weyl_inequality.