High-contrast homogenization: Entry.Analysis.SingularValueTheory

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Singular Value Theory

The singular values of a real square matrix: their definition and trace bound, the best rank-k approximation in the operator norm, the moment identity relating them to the Schatten norm, and their amplification under tensor powers. The trace and Schatten-moment bounds serve l.fixed.geometry.matrix.averaging; the rank approximation serves the Schatten ideal property consumed by p.fixed.geometry.parent.child.recurrence.

Singular values and the trace bound

Singular values of a real square matrix are square roots of its Gram eigenvalues. singularValues uses the original index type, without an order claim; singularValues₀ uses Mathlib's decreasing eigenvalue enumeration. The trace bound uses a Gram eigenbasis and scalar Cauchy–Schwarz, so it also applies to singular matrices and empty index types.

noncomputable def HCPolySupport.HighContrast.Analysis.singularValues {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (i : n) : ℝ

Singular values indexed by the original matrix index type, without an ordering claim.

Equations

• HCPolySupport.HighContrast.Analysis.singularValues X i = √(⋯.eigenvalues i)

noncomputable def HCPolySupport.HighContrast.Analysis.singularValues₀ {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (i : Fin (Fintype.card n)) : ℝ

Singular values in decreasing order, indexed from zero.

Equations

• HCPolySupport.HighContrast.Analysis.singularValues₀ X i = √(⋯.eigenvalues₀ i)

theorem HCPolySupport.HighContrast.Analysis.singularValues_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (i : n) : 0 ≤ singularValues X i

theorem HCPolySupport.HighContrast.Analysis.singularValues₀_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (i : Fin (Fintype.card n)) : 0 ≤ singularValues₀ X i

theorem HCPolySupport.HighContrast.Analysis.singularValues₀_antitone {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) : Antitone (singularValues₀ X)

theorem HCPolySupport.HighContrast.Analysis.sum_singularValues₀ {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (f : ℝ → ℝ) : ∑ i : Fin (Fintype.card n), f (singularValues₀ X i) = ∑ i : n, f (singularValues X i)

theorem HCPolySupport.HighContrast.Analysis.abs_trace_le_sum_singularValues {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) : |X.trace| ≤ ∑ i : n, singularValues X i

theorem HCPolySupport.HighContrast.Analysis.abs_trace_le_sum_singularValues₀ {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) : |X.trace| ≤ ∑ i : Fin (Fintype.card n), singularValues₀ X i

Approximation by matrices of bounded rank

The decreasing singular values, padded by zero, characterize approximation in the L2 operator norm. All statements allow an empty index type.

noncomputable def HCPolySupport.HighContrast.Analysis.singularValueAt {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (r : ℕ) : ℝ

The decreasing singular values, indexed from zero and padded by zero.

Equations

• HCPolySupport.HighContrast.Analysis.singularValueAt X r = if h : r < Fintype.card n then HCPolySupport.HighContrast.Analysis.singularValues₀ X ⟨r, h⟩ else 0

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (r : ℕ) : 0 ≤ singularValueAt X r

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_antitone {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) : Antitone (singularValueAt X)

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_eq_zero {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) {r : ℕ} (hr : Fintype.card n ≤ r) : singularValueAt X r = 0

theorem HCPolySupport.HighContrast.Analysis.rank_add_le {n : Type u_1} [Fintype n] (X Y : Matrix n n ℝ) : (X + Y).rank ≤ X.rank + Y.rank

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_le_norm_sub {n : Type u_1} [Fintype n] [DecidableEq n] (X R : Matrix n n ℝ) {r : ℕ} (hR : R.rank ≤ r) : singularValueAt X r ≤ ‖X - R‖

theorem HCPolySupport.HighContrast.Analysis.exists_rank_approximation {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) (r : ℕ) : ∃ (R : Matrix n n ℝ), R.rank ≤ r ∧ ‖X - R‖ ≤ singularValueAt X r

Singular moments and the Schatten norm

For a Hermitian matrix, the singular-value multiset is the absolute-value eigenvalue multiset. The proof compares characteristic polynomials; it does not assert that the two enumerations have the same order. The resulting moment identity identifies the generic singular norm with the Schatten norm on its intended Hermitian domain.

noncomputable def HCPolySupport.HighContrast.Analysis.singularNorm {n : Type u_1} [Fintype n] [DecidableEq n] (p : ℝ) (X : Matrix n n ℝ) : ℝ

The singular p-norm of an arbitrary real square matrix. Norm identities below require a positive exponent; no norm interpretation is asserted at p=0.

Equations

• HCPolySupport.HighContrast.Analysis.singularNorm p X = (∑ i : n, HCPolySupport.HighContrast.Analysis.singularValues X i ^ p) ^ p⁻¹

theorem HCPolySupport.HighContrast.Analysis.sum_eigenvalues_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.IsHermitian) (f g : ℝ → ℝ) (hf : (cfc f X).IsHermitian) : ∑ i : n, g (hf.eigenvalues i) = ∑ i : n, g (f (hX.eigenvalues i))

theorem HCPolySupport.HighContrast.Analysis.sum_singularValues_eq_abs_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.IsHermitian) (f : ℝ → ℝ) : ∑ i : n, f (singularValues X i) = ∑ i : n, f |hX.eigenvalues i|

theorem HCPolySupport.HighContrast.Analysis.singularNorm_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (p : ℝ) (X : Matrix n n ℝ) : 0 ≤ singularNorm p X

theorem HCPolySupport.HighContrast.Analysis.singularNorm_rpow {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) {p : ℝ} (hp : 0 < p) : singularNorm p X ^ p = ∑ i : n, singularValues X i ^ p

theorem HCPolySupport.HighContrast.Analysis.singularNorm_eq_absSchattenNorm {d : ℕ} {A : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) {p : ℝ} (hp : 1 ≤ p) : singularNorm p (toFullBlockMat A) = absSchattenNorm p A

Tensor amplification of singular norms

Finite tensor products preserve matrix multiplication and multiply traces and singular moments. All index types may be empty. In particular, the zeroth tensor power is the identity on the singleton type Fin 0 → n.

def HCPolySupport.HighContrast.Analysis.tensorPower {n : Type u_1} (X : Matrix n n ℝ) (q : ℕ) : Matrix (Fin q → n) (Fin q → n) ℝ

The tensor power on a function index type, including the scalar zeroth power.

Equations

• HCPolySupport.HighContrast.Analysis.tensorPower X q i j = ∏ k : Fin q, X (i k) (j k)

theorem HCPolySupport.HighContrast.Analysis.tensorPower_mul {n : Type u_1} [Fintype n] (X Y : Matrix n n ℝ) (q : ℕ) : tensorPower (X * Y) q = tensorPower X q * tensorPower Y q

theorem HCPolySupport.HighContrast.Analysis.tensorPower_one {n : Type u_1} [DecidableEq n] (q : ℕ) : tensorPower 1 q = 1

theorem HCPolySupport.HighContrast.Analysis.trace_tensorPower {n : Type u_1} [Fintype n] (X : Matrix n n ℝ) (q : ℕ) : (tensorPower X q).trace = X.trace ^ q

theorem HCPolySupport.HighContrast.Analysis.singularNorm_tensorPower {n : Type u_1} [Fintype n] [DecidableEq n] (X : Matrix n n ℝ) {p : ℝ} (hp : 0 < p) (q : ℕ) : singularNorm p (tensorPower X q) = singularNorm p X ^ q

theorem HCPolySupport.HighContrast.Analysis.tensorPower_prod {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (A : Fin N → Matrix n n ℝ) (q : ℕ) : tensorPower (List.ofFn A).prod q = (List.ofFn fun (k : Fin N) => tensorPower (A k) q).prod