High-contrast homogenization: Entry.Analysis.SchattenHolderInequalities

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

Schatten Holder Inequalities

The trace-Hölder inequality for non-commuting matrices, in Schatten norms. For N factors and their product A_1 ⋯ A_N it first establishes the dimension-free lossy bound |tr (A_1 ⋯ A_N)| ≤ N ∏ k, |A_k|_{S_N}, whose constant is the word length N rather than the matrix dimension, and then removes that loss to obtain the sharp bound |tr (A_1 ⋯ A_N)| ≤ ∏ k, |A_k|_{S_N}. The Hermitian block form of the sharp bound is the trace estimate consumed by the matrix-averaging step l.fixed.geometry.matrix.averaging; the file also records the elementary ingredients of the argument: the even trace identity tr(Y^N) = |Y|_{S_N}^N, the ℓ^p ⊆ ℓ^1 embedding, and finite Hölder with all exponents equal to N.

The even trace bridge, the ℓ^p ⊆ ℓ^1 embedding and finite Hölder

Three elementary ingredients of the printed proof of l.fixed.geometry.matrix.averaging, all deterministic:

• trace_even_pow_eq_absSchattenNorm_pow — for even N ≥ 2 and a symmetric block H, tr ((toFullBlockMat H) ^ N) = |H|_{S_N} ^ N, and that number is nonnegative. This is the print's "since N is even, tr(Y^N) = |Y|_{S_N}^N for every symmetric matrix Y". It is the existing HCPoly.Entry.Analysis.SchattenSpectral.absSchattenNorm_even_pow_eq_trace with the real index 2 * (k : ℝ) reconciled with the natural index N; the identity is already proved there and no eigenvalue sum is restated here.

• sum_rpow_le_rpow_sum — the ℓ^p ⊆ ℓ^1 embedding ∑ i, s i ^ p ≤ (∑ i, s i) ^ p for 1 ≤ p and nonnegative s. This is the step that turns a block-size exponent |B| / N into the printed 2 / N and |B| / 2, and it is exactly where "no singleton blocks" (2 ≤ |B|, hence 1 ≤ |B| / 2) is consumed.

• sum_prod_le_prod_sum_rpow — generalized finite Hölder for N nonnegative families with all exponents equal to N, proved by normalising each family to unit ℓ^N mass and applying weighted AM-GM (Real.geom_mean_le_arith_mean_weighted) with equal weights 1/N.

What this file does not contain, and why. Trace Hölder |tr (A_1 ⋯ A_N)| ≤ ∏ k, |A_k|_{S_N} for arbitrary noncommuting symmetric factors, is not proved here and is not stated here as a def, an axiom or a sorry. It is absent and is neither used nor assumed by any declaration in this file. The obstruction is genuine: even a constant-factor variant of the inequality does not hold. Nothing below depends on it.

The even trace identity

theorem HCPolySupport.HighContrast.Analysis.trace_even_pow_eq_absSchattenNorm_pow {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℕ} (hN : 2 ≤ N) (hNeven : Even N) : Matrix.trace (toFullBlockMat H ^ N) = absSchattenNorm (↑N) H ^ N

The even trace bridge. For an even natural N ≥ 2 and a symmetric block H, tr ((toFullBlockMat H) ^ N) = |H|_{S_N} ^ N. The print's sentence "since N is even, tr(Y^N) = |Y|_{S_N}^N for every symmetric matrix Y" (l.fixed.geometry.matrix.averaging).

Derived from absSchattenNorm_even_pow_eq_trace, which carries the real index 2 * (k : ℝ) and the natural power 2 * k; N = 2 * k with 1 ≤ k comes from hNeven and hN.

The ℓ^p ⊆ ℓ^1 embedding

theorem HCPolySupport.HighContrast.Analysis.sum_rpow_le_rpow_sum {ι : Type u_1} (t : Finset ι) (s : ι → ℝ) (hs : ∀ i ∈ t, 0 ≤ s i) {p : ℝ} (hp : 1 ≤ p) : ∑ i ∈ t, s i ^ p ≤ (∑ i ∈ t, s i) ^ p

ℓ^p ⊆ ℓ^1. For 1 ≤ p and nonnegative s, ∑ i ∈ t, s i ^ p ≤ (∑ i ∈ t, s i) ^ p (real rpow). Applied with p = |B| / 2 and 2 ≤ |B| this is the printed passage from a block of size |B| to the exponent |B| / 2 on the single sum ∑ i, (tr E[Y_i^N])^{2/N}.

Generalized finite Hölder for N families

theorem HCPolySupport.HighContrast.Analysis.sum_prod_le_prod_sum_rpow {ι : Type u_1} {N : ℕ} (hN : 0 < N) (t : Finset ι) (f : Fin N → ι → ℝ) (hf : ∀ (k : Fin N), ∀ i ∈ t, 0 ≤ f k i) : ∑ i ∈ t, ∏ k : Fin N, f k i ≤ ∏ k : Fin N, (∑ i ∈ t, f k i ^ ↑N) ^ (↑N)⁻¹

Generalized finite Hölder, all N exponents equal to N. For nonnegative families f 0, …, f (N-1) on a finset t, ∑ i ∈ t, ∏ k, f k i ≤ ∏ k, (∑ i ∈ t, f k i ^ N) ^ (1/N).

Route: if some family has zero ℓ^N mass it vanishes on t and both sides are 0; otherwise normalise each family to unit mass and apply weighted AM-GM with equal weights 1/N.

Lossy trace Holder for singular norms

This file proves the dimension-free lossy product bound used in the trace Holder route. The loss is the word length N, not the matrix dimension.

theorem HCPolySupport.HighContrast.Analysis.rank_prod_sub_prod_le {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (A C : Fin N → Matrix n n ℝ) : ((List.ofFn A).prod - (List.ofFn C).prod).rank ≤ ∑ k : Fin N, (A k - C k).rank

theorem HCPolySupport.HighContrast.Analysis.sum_block_bound {D N : ℕ} (hN : 0 < N) (u v : ℕ → ℝ) (hu : Antitone u) (hv : ∀ (i : ℕ), 0 ≤ v i) (h : ∀ (r : ℕ), u (N * r) ≤ v r) : ∑ i ∈ Finset.range D, u i ≤ ↑N * ∑ r ∈ Finset.range D, v r

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_prod_le {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (hN : 0 < N) (A : Fin N → Matrix n n ℝ) (r : ℕ) : singularValueAt (List.ofFn A).prod (N * r) ≤ ∏ k : Fin N, singularValueAt (A k) r

theorem HCPolySupport.HighContrast.Analysis.abs_trace_prod_le_card_mul_prod_singularNorm {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (hN : 0 < N) (A : Fin N → Matrix n n ℝ) : |(List.ofFn A).prod.trace| ≤ ↑N * ∏ k : Fin N, singularNorm (↑N) (A k)

Trace Holder for Schatten norms

This file removes the word-length constant in the lossy trace Holder bound by applying it to tensor powers and using Archimedean growth of powers.

theorem HCPolySupport.HighContrast.Analysis.le_of_all_pow_le_mul_pow {a b c : ℝ} (_ha : 0 ≤ a) (hb : 0 ≤ b) (_hc : 1 ≤ c) (h : ∀ (q : ℕ), a ^ q ≤ c * b ^ q) : a ≤ b

theorem HCPolySupport.HighContrast.Analysis.trace_prod_pow_le_card_mul_prod_singularNorm_pow {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (hN : 0 < N) (A : Fin N → Matrix n n ℝ) (q : ℕ) : |(List.ofFn A).prod.trace| ^ q ≤ ↑N * (∏ k : Fin N, singularNorm (↑N) (A k)) ^ q

theorem HCPolySupport.HighContrast.Analysis.abs_trace_prod_le_prod_singularNorm {n : Type u_1} [Fintype n] [DecidableEq n] {N : ℕ} (hN : 0 < N) (A : Fin N → Matrix n n ℝ) : |(List.ofFn A).prod.trace| ≤ ∏ k : Fin N, singularNorm (↑N) (A k)

theorem HCPolySupport.HighContrast.Analysis.abs_trace_prod_le_prod_absSchattenNorm {d N : ℕ} (hN : 2 ≤ N) (A : Fin N → BlockMat d) (hA : ∀ (k : Fin N), Matrix.IsHermitian (toFullBlockMat (A k))) : |Matrix.trace (List.ofFn fun (k : Fin N) => toFullBlockMat (A k)).prod| ≤ ∏ k : Fin N, absSchattenNorm (↑N) (A k)