High-contrast homogenization: Entry.Analysis.SchattenCongruence

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

The sharp Schatten congruence bound

p.fixed.geometry.parent.child.recurrence invokes the Schatten ideal property. Rank approximation in the L2 operator norm proves singular-value domination for arbitrary real congruence matrices, including singular matrices and zero. Summing powers gives the exact deterministic coefficient; integrating genuine finite moments gives the law-level bound with the same coefficient.

The approximation-number and singular-moment libraries are the committed K1 infrastructure consumed at No separate Courant–Fischer construction is needed: exists_rank_approximation and singularValueAt_le_norm_sub already provide the required comparison. No Loewner monotonicity of the absolute value or square is used. The independent congruence-order bridges remain available below.

theorem HCPolySupport.HighContrast.Analysis.matrix_congr_le {ι : Type u_1} [Fintype ι] {A B : Matrix ι ι ℝ} (hAB : A ≤ B) (S : Matrix ι ι ℝ) : S.transpose * A * S ≤ S.transpose * B * S

Congruence by any real matrix preserves the Loewner order: no Hermitian, invertibility or nonsingularity hypothesis on S, so S = 0 (the printed "degenerate B" case) specializes to 0 ≤ 0 with no case split. Public replacement for the private HCPoly.Entry.Multiscale.DriftAdvance.matrix_congr_le, which this file does not and cannot reach into.

theorem HCPolySupport.HighContrast.Analysis.matrixOrder_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) (hB : Matrix.IsHermitian (toFullBlockMat B)) (hAB : BlockMatLoewnerLE A B) : toFullBlockMat A ≤ toFullBlockMat B

BlockMatLoewnerLE plus Hermitian symmetry of both sides transports to the ambient Matrix Loewner order on toFullBlockMat. Same construction as the private HCPoly.Entry.Multiscale.DriftAdvance.matrixOrder_of_blockMatLoewnerLE, reproved here so this file does not reach into another file's private namespace.

theorem HCPolySupport.HighContrast.Analysis.blockMatLoewnerLE_of_le {d : ℕ} {M N : FullBlockMat d} (hMN : M ≤ N) : BlockMatLoewnerLE (ofFullBlockMat M) (ofFullBlockMat N)

The reverse bridge: an ambient Matrix Loewner inequality between two doubled blocks' full representations gives BlockMatLoewnerLE of the (ofFullBlockMat-recovered) blocks.

theorem HCPolySupport.HighContrast.Analysis.blockMatLoewnerLE_congr_le {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hAB : BlockMatLoewnerLE A B) (S : FullBlockMat d) : BlockMatLoewnerLE (ofFullBlockMat (Matrix.transpose S * toFullBlockMat A * S)) (ofFullBlockMat (Matrix.transpose S * toFullBlockMat B * S))

The BlockMat/BlockMatLoewnerLE transport of matrix_congr_le: congruence by any FullBlockMat d (via toFullBlockMat/ofFullBlockMat) preserves the doubled-block Loewner order, given both sides are symmetric doubled blocks.

theorem HCPolySupport.HighContrast.Analysis.singularValueAt_congr_le {n : Type u_1} [Fintype n] [DecidableEq n] (X B : Matrix n n ℝ) (r : ℕ) : singularValueAt (B.transpose * X * B) r ≤ ‖B‖ ^ 2 * singularValueAt X r

Rank approximation gives singular-value domination under arbitrary congruence.

theorem HCPolySupport.HighContrast.Analysis.singularNorm_congr_le {n : Type u_1} [Fintype n] [DecidableEq n] (X B : Matrix n n ℝ) {p : ℝ} (hp : 0 < p) : singularNorm p (B.transpose * X * B) ≤ ‖B‖ ^ 2 * singularNorm p X

Congruence is bounded on every positive singular p-norm.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_congr_le {d : ℕ} (X : BlockMat d) (B : FullBlockMat d) (hX : Matrix.IsHermitian (toFullBlockMat X)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N (ofFullBlockMat (Matrix.transpose B * toFullBlockMat X * B)) ≤ ‖B‖ ^ 2 * absSchattenNorm N X

The sharp Schatten ideal estimate, including singular congruence matrices.

theorem HCPolySupport.HighContrast.Analysis.lqSchattenNorm_congr_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (B : FullBlockMat d) : (lqSchattenNorm P N fun (a : CoeffSpace d) => ofFullBlockMat (Matrix.transpose B * toFullBlockMat (H a) * B)) ≤ ‖B‖ ^ 2 * lqSchattenNorm P N H

Integrating the sharp pointwise estimate preserves its dimension-free coefficient.