High-contrast homogenization: Entry.Analysis.SchattenNormIntegrability

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

Schatten Norm Integrability

Integrability and measurability of the Schatten norm of a random matrix, and the membership predicate the moment estimates are stated with.

It serves l.fixed.geometry.positive.gap, whose mixed-norm moment estimate is stated with this carrier, and l.fixed.geometry.matrix.averaging, whose product-integrability bridge uses the entrywise operator-norm bound.

Integrability support for the positive-gap estimate

This file collects the supporting lemmas for the positive-gap estimate: entrywise expectations, trace/order preservation by integration, and basic membership examples.

theorem HCPolySupport.HighContrast.SchattenMemLp.memLp_absSchattenNorm {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (hN : 1 ≤ N) : MeasureTheory.MemLp (fun (a : CoeffSpace d) => absSchattenNorm N (H a)) (ENNReal.ofReal N) P

The real Schatten moment carrier gives the corresponding Mathlib eLpNorm membership of the scalar Schatten norm.

theorem HCPolySupport.HighContrast.SchattenMemLp.lqSchattenNorm_eq_eLpNorm_toReal {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (hN : 1 ≤ N) : MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => absSchattenNorm N (H a)) (ENNReal.ofReal N) P < ⊤ ∧ 0 ≤ lqSchattenNorm P N H ∧ lqSchattenNorm P N H = (MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => absSchattenNorm N (H a)) (ENNReal.ofReal N) P).toReal

The real mixed norm is the real value of the finite Mathlib eLpNorm.

theorem HCPolySupport.HighContrast.SchattenMemLp.abs_blockMatEntry_le_blockOpNorm {d : ℕ} (H : BlockMat d) (α β : BlockCoord d) : |blockMatEntry H α β| ≤ blockOpNorm H

theorem HCPolySupport.HighContrast.SchattenMemLp.integrable_entry {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℝ} {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (hN : 1 ≤ N) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (H a) α β) P

Each scalar block entry is integrable on a finite measure space.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_le_dim_rpow_mul_blockOpNorm {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N H ≤ (2 * ↑d) ^ N⁻¹ * blockOpNorm H

A crude finite-dimensional comparison in the reverse direction from blockOpNorm_le_absSchattenNorm. The factor depends only on the doubled block dimension and the exponent; it is used only to prove membership/definedness of subtraction and centering fields, not as one of the sharp printed constants in the PositiveGap estimate.

theorem HCPolySupport.HighContrast.Analysis.memLqSchatten_const {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsFiniteMeasure P] {N : ℝ} (_hN : 1 ≤ N) (B : BlockMat d) (hB : IsSymmetricBlockMat B) : SchattenMemLp P N fun (x : CoeffSpace d) => B

Constant symmetric blocks are in the real Schatten carrier over a finite law.

theorem HCPolySupport.HighContrast.Analysis.integral_blockSub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {F G : CoeffSpace d → BlockMat d} (hF : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (F a) α β) P) (hG : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (G a) α β) P) : ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (blockSub (F a) (G a)) α β ∂P) = blockSub (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P)) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P))

Entrywise Bochner integration commutes with block subtraction.

theorem HCPolySupport.HighContrast.Analysis.blockTrace_integral {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {H : CoeffSpace d → BlockMat d} (hH : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (H a) α β) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockTrace (H a)) P ∧ blockTrace (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (H a) α β ∂P)) = ∫ (a : CoeffSpace d), blockTrace (H a) ∂P

The trace of an entrywise Bochner expectation is the expected trace.

theorem HCPolySupport.HighContrast.Analysis.isSymmetricBlockMat_integral {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {H : CoeffSpace d → BlockMat d} (hH : ∀ᵐ (a : CoeffSpace d) ∂P, IsSymmetricBlockMat (H a)) : IsSymmetricBlockMat (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (H a) α β ∂P))

Entrywise Bochner expectation preserves almost-everywhere symmetry.

theorem HCPolySupport.HighContrast.Analysis.blockMatLoewnerLE_integral {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {F G : CoeffSpace d → BlockMat d} (hF : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (F a) α β) P) (hG : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (G a) α β) P) (hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a)) : BlockMatLoewnerLE (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P)) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P))

Entrywise Bochner expectation preserves the block Loewner order.

Measurability and membership closure for the Schatten norm

EccentricityScaleDecay for the paper's Schatten estimates, on the real exponent and CG block carriers. The pinned Mathlib supplies the real matrix CFC, but does not register its isometry for the L2 operator norm. We prove that property from the spectral representation, then use Mathlib's variable-operator continuity.

Continuity is asserted on symmetric full matrices. The CFC is zero off that closed set, so its Schatten value is measurable on all full matrices. Entrywise a.e. measurability therefore suffices, without a circular moment premise. The dimension factor in the subtraction proof proves finiteness only; it is not a sharp Schatten triangle inequality or a constant in the printed gap estimate.

theorem HCPolySupport.HighContrast.Analysis.continuousOn_absSchattenNorm {d : ℕ} {N : ℝ} (hN : 1 ≤ N) : ContinuousOn (fun (M : FullBlockMat d) => absSchattenNorm N (ofFullBlockMat M)) {M : FullBlockMat d | Matrix.IsHermitian M}

The Schatten norm is continuous on symmetric full blocks, for every real exponent N ≥ 1, including nonintegral exponents and dimension zero.

theorem HCPolySupport.HighContrast.Analysis.measurable_absSchattenNorm {d : ℕ} {N : ℝ} (hN : 1 ≤ N) : Measurable fun (M : BlockCoord d → BlockCoord d → ℝ) => absSchattenNorm N (ofFullBlockMat M)

Borel measurability on all full blocks uses the zero convention off the closed set of symmetric matrices; global continuity is not asserted. The explicit function type is CG's FullBlockMat d unfolded to expose its entrywise Borel sigma algebra, without adding an instance or a carrier.

theorem HCPolySupport.HighContrast.Analysis.aestronglyMeasurable_absSchattenNorm {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {F : CoeffSpace d → BlockMat d} (hF : HasMeasurableBlock P F) {N : ℝ} (hN : 1 ≤ N) : MeasureTheory.AEStronglyMeasurable (fun (ω : CoeffSpace d) => absSchattenNorm N (F ω)) P

The a.e. measurability bridge depends on the entrywise measurability premise alone, so it applies in particular to a.e. symmetric fields before their moment integrability has been established.

theorem HCPolySupport.HighContrast.SchattenMemLp.sub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {F G : CoeffSpace d → BlockMat d} (hF : SchattenMemLp P N F) (hG : SchattenMemLp P N G) (hN : 1 ≤ N) : SchattenMemLp P N fun (a : CoeffSpace d) => blockSub (F a) (G a)

Subtraction preserves the real Schatten moment carrier on any measure space. The crude factor (2*d)^(1/N) is used only for moment finiteness, and does not supply the sharp triangle inequality in the printed gap estimate.

theorem HCPolySupport.HighContrast.SchattenMemLp.center {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℝ} {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (hN : 1 ≤ N) : SchattenMemLp P N fun (a : CoeffSpace d) => blockSub (H a) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (H b) α β ∂P))

Centering by the entrywise expectation preserves membership on a finite measure space. This uses subtraction closure and symmetry of the mean, with no additional moment or measurability premise.