Majorization and weak log-majorization

This file develops the theory of majorization for finite sequences, leading to the key singular value inequality needed for the Schatten–Hölder inequality.

Main results

• sum_rpow_singularValues_mul_le: for r > 0, the singular values of A * B satisfy ∑ σᵢ(AB)^r ≤ ∑ σ↓ᵢ(A)^r · σ↓ᵢ(B)^r.
• holder_step_for_singularValues: the Hölder step giving ∑ σ↓ᵢ(A)^r · σ↓ᵢ(B)^r ≤ (∑ σᵢ(A)^p)^{r/p} · (∑ σᵢ(B)^q)^{r/q}.

Sorted singular values

def singularValues {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) : d → ℝ

The singular values of a square complex matrix A, defined as the square roots of the eigenvalues of A†A. These are indexed by d without a particular ordering.

Note: We use A.conjTranspose as the argument to isHermitian_mul_conjTranspose_self so that the underlying Hermitian matrix is A† * A (matching the convention in schattenNorm).

Equations

• singularValues A i = √(⋯.eigenvalues i)

theorem singularValues_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (i : d) : 0 ≤ singularValues A i

Singular values are nonneg.

noncomputable def singularValuesSorted {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) : Fin (Fintype.card d) → ℝ

The sorted singular values of a square complex matrix, in decreasing order, indexed by Fin (Fintype.card d).

We define them by sorting the multiset of singular values.

Equations

• singularValuesSorted A i = ((Multiset.map (singularValues A) Finset.univ.val).sort fun (x1 x2 : ℝ) => x1 ≥ x2).get ⟨↑i, ⋯⟩

theorem singularValuesSorted_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (i : Fin (Fintype.card d)) : 0 ≤ singularValuesSorted A i

Sorted singular values are nonneg.

theorem sum_singularValues_rpow_eq_sum_sorted {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (p : ℝ) : ∑ i : d, singularValues A i ^ p = ∑ i : Fin (Fintype.card d), singularValuesSorted A i ^ p

The sum ∑ singularValues A i ^ p equals the sum over sorted singular values.

Weak log-majorization and its consequences

theorem singularValuesSorted_antitone {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) : Antitone (singularValuesSorted A)

Sorted singular values are antitone (decreasing).

theorem antitone_mul_of_antitone_nonneg {n : ℕ} {f g : Fin n → ℝ} (hf : Antitone f) (hg : Antitone g) (hf_nn : ∀ (i : Fin n), 0 ≤ f i) (hg_nn : ∀ (i : Fin n), 0 ≤ g i) : Antitone fun (i : Fin n) => f i * g i

The product of nonneg antitone sequences is antitone.

Compound matrices and auxiliary lemmas for Horn's inequality

The proof of Horn's inequality uses the compound matrix (or k-th exterior power of a matrix). For a d × d matrix M and k ≤ card d, the k-th compound matrix C_k(M) is indexed by k-element subsets of the index type, with entry (S, T) being the minor det M[S, T].

The key properties are:

1. Cauchy–Binet: C_k(M N) = C_k(M) · C_k(N).
2. Spectral characterisation: the largest singular value of C_k(M) is ∏_{i=1}^k σ↓ᵢ(M).
3. Operator-norm submultiplicativity: σ₁(A B) ≤ σ₁(A) · σ₁(B).

Combining these gives Horn's inequality: ∏ σ↓(AB) = σ₁(C_k(AB)) = σ₁(C_k(A) C_k(B)) ≤ σ₁(C_k(A)) σ₁(C_k(B)) = (∏ σ↓(A))(∏ σ↓(B)).

def AllOrdered.fintypeLinearOrderClassical (α : Type u_2) [Fintype α] [DecidableEq α] : LinearOrder α

A LinearOrder on any Fintype, obtained classically via well-ordering.

Equations

• AllOrdered.fintypeLinearOrderClassical α = linearOrderOfSTO WellOrderingRel

noncomputable def compoundMatrix {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) : Matrix { S : Finset d // S.card = k } { S : Finset d // S.card = k } ℂ

The k-th compound (exterior-power) matrix of M.

Equations

• compoundMatrix M k S T = (M.submatrix (fun (i : Fin k) => ((↑S).orderEmbOfFin ⋯) i) fun (j : Fin k) => ((↑T).orderEmbOfFin ⋯) j).det

theorem cauchyBinet {m : ℕ} {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrder n] {R : Type u_3} [CommRing R] (A : Matrix (Fin m) n R) (B : Matrix n (Fin m) R) : (A * B).det = ∑ S : { S : Finset n // S.card = m }, (A.submatrix id ⇑((↑S).orderEmbOfFin ⋯)).det * (B.submatrix (⇑((↑S).orderEmbOfFin ⋯)) id).det

Cauchy–Binet formula for rectangular matrices: if A is m × n and B is n × m, then det(A * B) = ∑_S det(A[:,S]) * det(B[S,:]) where the sum is over m-element subsets S of the column/row index.

theorem compoundMatrix_mul {d : Type u_1} [Fintype d] [DecidableEq d] (M N : Matrix d d ℂ) (k : ℕ) : compoundMatrix (M * N) k = compoundMatrix M k * compoundMatrix N k

The compoundMatrix of a product is the product of the compoundMatrixs.

theorem compoundMatrix_conjTranspose {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) : compoundMatrix M.conjTranspose k = (compoundMatrix M k).conjTranspose

compoundMatrix commutes with conjTranspose.

theorem compoundMatrix_diagonal {d : Type u_1} [Fintype d] [DecidableEq d] (f : d → ℂ) (k : ℕ) : compoundMatrix (Matrix.diagonal f) k = Matrix.diagonal fun (S : { S : Finset d // S.card = k }) => ∏ i : Fin k, f (((↑S).orderEmbOfFin ⋯) i)

The compound matrix of a diagonal matrix is diagonal, with entries being products of eigenvalues over k-subsets.

theorem singularValues_compoundMatrix_eq {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) (S : { S : Finset d // S.card = k }) : ∃ (j : { S : Finset d // S.card = k }), singularValues (compoundMatrix M k) j = ∏ i : Fin k, singularValues M (((↑S).orderEmbOfFin ⋯) i)

The eigenvalues of the compound matrix of a Hermitian matrix are the products of eigenvalues over k-subsets. More precisely, the singular values of compoundMatrix M k are the square roots of products of eigenvalues of M†M over k-subsets.

theorem prod_le_prod_sorted {n : ℕ} {f : Fin n → ℝ} (hf : Antitone f) (hf_nn : ∀ (i : Fin n), 0 ≤ f i) (k : ℕ) (hk : k ≤ n) (g : Fin k → Fin n) (hg : Function.Injective g) : ∏ i : Fin k, f (g i) ≤ ∏ i : Fin k, f ⟨↑i, ⋯⟩

The product of nonneg values over a k-subset is at most the product of the k largest values.

theorem singularValuesSorted_zero_eq_sup {e : Type u_2} [Fintype e] [DecidableEq e] (A : Matrix e e ℂ) (h : 0 < Fintype.card e) : singularValuesSorted A ⟨0, h⟩ = Finset.univ.sup' ⋯ (singularValues A)

The 0th sorted singular value is the maximum of the singular values.

theorem singularValues_mem_sorted {e : Type u_2} [Fintype e] [DecidableEq e] (A : Matrix e e ℂ) (i : e) : ∃ (j : Fin (Fintype.card e)), singularValues A i = singularValuesSorted A j

Each singular value appears in the sorted list.

theorem singularValuesSorted_mem_values {e : Type u_2} [Fintype e] [DecidableEq e] (A : Matrix e e ℂ) (j : Fin (Fintype.card e)) : ∃ (i : e), singularValuesSorted A j = singularValues A i

Each sorted singular value appears among the original singular values.

theorem singularValues_compoundMatrix_perm {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) : ∃ (σ : { S : Finset d // S.card = k } ≃ { S : Finset d // S.card = k }), ∀ (S : { S : Finset d // S.card = k }), singularValues (compoundMatrix M k) (σ S) = ∏ i : Fin k, singularValues M (((↑S).orderEmbOfFin ⋯) i)

Stronger version of singularValues_compoundMatrix_eq that exposes the permutation.

theorem singularValues_compoundMatrix_rev {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) (j : { S : Finset d // S.card = k }) : ∃ (S : { S : Finset d // S.card = k }), singularValues (compoundMatrix M k) j = ∏ i : Fin k, singularValues M (((↑S).orderEmbOfFin ⋯) i)

Converse of singularValues_compoundMatrix_eq: every singular value of the compound matrix is a product of singular values of M over some k-subset.

theorem exists_sorting_equiv {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) : ∃ (σ : Fin (Fintype.card d) ≃ d), ∀ (i : Fin (Fintype.card d)), singularValues M (σ i) = singularValuesSorted M i

There exists a bijection σ : Fin (card d) ≃ d such that singularValues M (σ i) = singularValuesSorted M i for all i.

theorem prod_singularValues_subset_le_sorted_prod {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) (hk : k ≤ Fintype.card d) (S : { S : Finset d // S.card = k }) : ∏ i : Fin k, singularValues M (((↑S).orderEmbOfFin ⋯) i) ≤ ∏ i : Fin k, singularValuesSorted M ⟨↑i, ⋯⟩

For any k-subset S of d, the product of singular values over S is ≤ the product of the top k sorted singular values.

theorem exists_subset_prod_eq_sorted_prod {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) (hk : k ≤ Fintype.card d) : ∃ (S : { S : Finset d // S.card = k }), ∏ i : Fin k, singularValues M (((↑S).orderEmbOfFin ⋯) i) = ∏ i : Fin k, singularValuesSorted M ⟨↑i, ⋯⟩

theorem prod_singularValuesSorted_eq_compoundSV {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (k : ℕ) (hk : k ≤ Fintype.card d) : ∏ i : Fin k, singularValuesSorted M ⟨↑i, ⋯⟩ = singularValuesSorted (compoundMatrix M k) ⟨0, ⋯⟩

theorem IsHermitian.inner_le_sup_eigenvalue_mul_inner {e : Type u_2} [Fintype e] [DecidableEq e] (H : Matrix e e ℂ) (hH : H.IsHermitian) (he : 0 < Fintype.card e) (v : e → ℂ) : (star v ⬝ᵥ H.mulVec v).re ≤ Finset.univ.sup' ⋯ hH.eigenvalues * (star v ⬝ᵥ v).re

The Rayleigh quotient bound: For a Hermitian matrix H with eigenvalues λ, we have v† H v ≤ (max λ) · v† v for all v.

theorem eigenvalue_le_singularValuesSorted_sq {e : Type u_2} [Fintype e] [DecidableEq e] (A : Matrix e e ℂ) (h : 0 < Fintype.card e) (i : e) : ⋯.eigenvalues i ≤ singularValuesSorted A ⟨0, h⟩ ^ 2

theorem quadratic_form_le_singularValuesSorted_sq {e : Type u_2} [Fintype e] [DecidableEq e] (A : Matrix e e ℂ) (h : 0 < Fintype.card e) (v : e → ℂ) : (star v ⬝ᵥ (A.conjTranspose * A).mulVec v).re ≤ singularValuesSorted A ⟨0, h⟩ ^ 2 * (star v ⬝ᵥ v).re

The quadratic form of A† A is bounded by (max singular value)² * ‖v‖².

theorem singularValuesSorted_mul_le {e : Type u_2} [Fintype e] [DecidableEq e] (M N : Matrix e e ℂ) (h : 0 < Fintype.card e) : singularValuesSorted (M * N) ⟨0, h⟩ ≤ singularValuesSorted M ⟨0, h⟩ * singularValuesSorted N ⟨0, h⟩

The largest singular value of a matrix product is at most the product of the largest singular values: σ₁(M * N) ≤ σ₁(M) * σ₁(N). This is operator-norm submultiplicativity.

theorem horn_weak_log_majorization {d : Type u_1} [Fintype d] [DecidableEq d] (A B : Matrix d d ℂ) (k : ℕ) (hk : k ≤ Fintype.card d) : ∏ i : Fin k, singularValuesSorted (A * B) ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, singularValuesSorted A ⟨↑i, ⋯⟩ * singularValuesSorted B ⟨↑i, ⋯⟩

Horn's inequality (weak log-majorization of singular values): For all k, ∏_{i<k} σ↓ᵢ(AB) ≤ ∏_{i<k} σ↓ᵢ(A) · σ↓ᵢ(B). This follows from submultiplicativity of the operator norm applied to exterior powers of the matrices.

Weak log-majorization implies sum of powers inequality

theorem rpow_antitone_of_nonneg_antitone {n : ℕ} {f : Fin n → ℝ} (hf : Antitone f) (hf_nn : ∀ (i : Fin n), 0 ≤ f i) {r : ℝ} (hr : 0 < r) : Antitone fun (i : Fin n) => f i ^ r

Raising nonneg antitone sequences to a positive power preserves antitonicity.

theorem rpow_preserves_weak_log_maj {n : ℕ} {x y : Fin n → ℝ} (hx_nn : ∀ (i : Fin n), 0 ≤ x i) (hy_nn : ∀ (i : Fin n), 0 ≤ y i) (h_log_maj : ∀ (k : ℕ) (x_1 : k ≤ n), ∏ i : Fin k, x ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, y ⟨↑i, ⋯⟩) {r : ℝ} (hr : 0 < r) (k : ℕ) (x✝ : k ≤ n) : ∏ i : Fin k, (fun (j : Fin n) => x j ^ r) ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, (fun (j : Fin n) => y j ^ r) ⟨↑i, ⋯⟩

Weak log-majorization is preserved under positive powers.

theorem sum_mul_log_nonneg_of_weak_log_maj {n : ℕ} {x y : Fin n → ℝ} (hx_pos : ∀ (i : Fin n), 0 < x i) (hy_pos : ∀ (i : Fin n), 0 < y i) (hx_anti : Antitone x) (h_log_maj : ∀ (k : ℕ) (x_1 : k ≤ n), ∏ i : Fin k, x ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, y ⟨↑i, ⋯⟩) : 0 ≤ ∑ i : Fin n, x i * Real.log (y i / x i)

theorem sub_ge_mul_log_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : b - a ≥ a * Real.log (b / a)

theorem weak_log_maj_sum_le {n : ℕ} {x y : Fin n → ℝ} (hx_nn : ∀ (i : Fin n), 0 ≤ x i) (hy_nn : ∀ (i : Fin n), 0 ≤ y i) (hx_anti : Antitone x) (hy_anti : Antitone y) (h_log_maj : ∀ (k : ℕ) (x_1 : k ≤ n), ∏ i : Fin k, x ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, y ⟨↑i, ⋯⟩) : ∑ i : Fin n, x i ≤ ∑ i : Fin n, y i

theorem weak_log_maj_sum_rpow_le {n : ℕ} {x y : Fin n → ℝ} (hx_nn : ∀ (i : Fin n), 0 ≤ x i) (hy_nn : ∀ (i : Fin n), 0 ≤ y i) (hx_anti : Antitone x) (hy_anti : Antitone y) (h_log_maj : ∀ (k : ℕ) (x_1 : k ≤ n), ∏ i : Fin k, x ⟨↑i, ⋯⟩ ≤ ∏ i : Fin k, y ⟨↑i, ⋯⟩) {r : ℝ} (hr : 0 < r) : ∑ i : Fin n, x i ^ r ≤ ∑ i : Fin n, y i ^ r

Weak log-majorization of nonneg antitone sequences implies the sum of powers inequality.

Key singular value inequality for products

theorem sum_rpow_singularValues_mul_le {d : Type u_1} [Fintype d] [DecidableEq d] (A B : Matrix d d ℂ) {r : ℝ} (hr : 0 < r) : ∑ i : Fin (Fintype.card d), singularValuesSorted (A * B) i ^ r ≤ ∑ i : Fin (Fintype.card d), singularValuesSorted A i ^ r * singularValuesSorted B i ^ r

Hölder inequality for singular values

theorem holder_step_for_singularValues {d : Type u_1} [Fintype d] [DecidableEq d] (A B : Matrix d d ℂ) {r p q : ℝ} (hr : 0 < r) (hp : 0 < p) (hq : 0 < q) (hpqr : 1 / r = 1 / p + 1 / q) : ∑ i : Fin (Fintype.card d), singularValuesSorted A i ^ r * singularValuesSorted B i ^ r ≤ (∑ i : Fin (Fintype.card d), singularValuesSorted A i ^ p) ^ (r / p) * (∑ i : Fin (Fintype.card d), singularValuesSorted B i ^ q) ^ (r / q)

The finite-sum Hölder inequality applied to sequences of r-th powers of sorted singular values.

With conjugate exponents p' = p/r > 1 and q' = q/r > 1 (which satisfy 1/p' + 1/q' = 1 when 1/r = 1/p + 1/q), this gives: ∑ σ↓ᵢ(A)^r · σ↓ᵢ(B)^r ≤ (∑ σ↓ᵢ(A)^p)^{r/p} · (∑ σ↓ᵢ(B)^q)^{r/q}

Note: The sums on the RHS don't depend on the ordering, so we can replace sorted singular values with unsorted ones.