High-contrast homogenization: Entry.Analysis.SchattenNormFoundations

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

Schatten Norm Foundations

The deterministic Schatten norm: its spectral formula, the diagonal Hölder bound in an orthogonal basis, and the triangle inequality. These deterministic estimates serve the finite-range matrix averaging lemma l.fixed.geometry.matrix.averaging, through the even trace-power identity and the spectral formula, and the positive-gap lemma l.fixed.geometry.positive.gap, through the trace and operator-norm comparisons and the triangle inequality.

Spectral facts for the Schatten norm

This file discharges the deterministic spectral bridge for the real-valued Schatten norm of HCPoly/Entry/Setup/SchattenNorm.lean.

theorem HCPolySupport.HighContrast.Analysis.toFullBlockMat_isHermitian_iff {d : ℕ} (H : BlockMat d) : Matrix.IsHermitian (toFullBlockMat H) ↔ IsSymmetricBlockMat H

theorem HCPolySupport.HighContrast.Analysis.trace_cfc_abs_rpow_eq_sum {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (_hN : 1 ≤ N) : (cfc (fun (x : ℝ) => |x| ^ N) (toFullBlockMat H)).trace = ∑ i : BlockCoord d, |hH.eigenvalues i| ^ N

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_eq_eigenvalues {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} : absSchattenNorm N H = schattenNormEigen hH N

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_nonneg {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (_hN : 1 ≤ N) : 0 ≤ absSchattenNorm N H

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_rpow_eq_sum {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N H ^ N = ∑ i : BlockCoord d, |hH.eigenvalues i| ^ N

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_even_pow_eq_trace {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) (k : ℕ) (hk : 1 ≤ k) : absSchattenNorm (2 * ↑k) H ^ (2 * k) = Matrix.trace (toFullBlockMat H ^ (2 * k))

theorem HCPolySupport.HighContrast.Analysis.blockTrace_nonneg {d : ℕ} {H : BlockMat d} (hH : Matrix.PosSemidef (toFullBlockMat H)) : 0 ≤ blockTrace H

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_one_eq_blockTrace {d : ℕ} {H : BlockMat d} (hH : Matrix.PosSemidef (toFullBlockMat H)) : absSchattenNorm 1 H = blockTrace H

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_le_blockTrace {d : ℕ} {H : BlockMat d} (hH : Matrix.PosSemidef (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N H ≤ blockTrace H

theorem HCPolySupport.HighContrast.Analysis.blockOpNorm_le_absSchattenNorm {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) : blockOpNorm H ≤ absSchattenNorm N H

theorem HCPolySupport.HighContrast.Analysis.blockTrace_le_dim_mul_blockOpNorm {d : ℕ} {H : BlockMat d} (hH : Matrix.PosSemidef (toFullBlockMat H)) : blockTrace H ≤ 2 * ↑d * blockOpNorm H

Diagonal estimates in orthogonal bases

Squared entries of a real unitary matrix have row and column sums one. Weighted scalar Hölder therefore bounds the diagonal in any orthogonal basis by the spectral Schatten value. No commutation of the matrices is used.

theorem HCPolySupport.HighContrast.Analysis.unitary_sum_sq_row {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(unitary (Matrix n n ℝ))) (i : n) : ∑ j : n, ↑U i j ^ 2 = 1

theorem HCPolySupport.HighContrast.Analysis.unitary_sum_sq_col {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(unitary (Matrix n n ℝ))) (j : n) : ∑ i : n, ↑U i j ^ 2 = 1

theorem HCPolySupport.HighContrast.Analysis.unitary_conj_diagonal_apply {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(unitary (Matrix n n ℝ))) (f : n → ℝ) (i : n) : ((Unitary.conjStarAlgAut ℝ (Matrix n n ℝ)) U) (Matrix.diagonal f) i i = ∑ j : n, ↑U i j ^ 2 * f j

theorem HCPolySupport.HighContrast.Analysis.hermitian_conj_diagonal_eq {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (U : ↥(unitary (Matrix n n ℝ))) (i : n) : ((Unitary.conjStarAlgAut ℝ (Matrix n n ℝ)) U) A i i = ∑ j : n, ↑(U * hA.eigenvectorUnitary) i j ^ 2 * hA.eigenvalues j

theorem HCPolySupport.HighContrast.Analysis.hermitian_norm_eq_eigenvalue_norm {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) : ‖A‖ = ‖hA.eigenvalues‖

theorem HCPolySupport.HighContrast.Analysis.hermitian_conj_diagonal_le_norm {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (U : ↥(unitary (Matrix n n ℝ))) (i : n) : ((Unitary.conjStarAlgAut ℝ (Matrix n n ℝ)) U) A i i ≤ ‖A‖

theorem HCPolySupport.HighContrast.Analysis.unitary_diagonal_rpow_le {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(unitary (Matrix n n ℝ))) (f : n → ℝ) {N : ℝ} (hN : 1 ≤ N) (i : n) : |∑ j : n, ↑U i j ^ 2 * f j| ^ N ≤ ∑ j : n, ↑U i j ^ 2 * |f j| ^ N

theorem HCPolySupport.HighContrast.Analysis.hermitian_sum_diagonal_rpow_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (U : ↥(unitary (Matrix n n ℝ))) {N : ℝ} (hN : 1 ≤ N) : ∑ i : n, |((Unitary.conjStarAlgAut ℝ (Matrix n n ℝ)) U) A i i| ^ N ≤ ∑ j : n, |hA.eigenvalues j| ^ N

The Schatten triangle inequality for symmetric real blocks

Diagonalize the sum, apply scalar Minkowski to its diagonal entries, and bound the diagonal of each summand by weighted Hölder. This proves coefficient one for noncommuting signed symmetric matrices and every real exponent N ≥ 1.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_add_le {d : ℕ} {A B : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) (hB : Matrix.IsHermitian (toFullBlockMat B)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N (ofFullBlockMat (toFullBlockMat A + toFullBlockMat B)) ≤ absSchattenNorm N A + absSchattenNorm N B

Full triangle inequality, including the trace-norm endpoint and empty blocks.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_neg {d : ℕ} {A : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N (ofFullBlockMat (-toFullBlockMat A)) = absSchattenNorm N A

Invariance under negation, obtained by applying the diagonal estimate twice.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_sub_le {d : ℕ} {A B : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) (hB : Matrix.IsHermitian (toFullBlockMat B)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N (blockSub A B) ≤ absSchattenNorm N A + absSchattenNorm N B

Subtraction form consumed by the centering step.