High-contrast homogenization: Entry.PositiveGap

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

The positive-gap lemma

Proves the real-exponent, almost-everywhere statement near l.fixed.geometry.positive.gap by nonlinear interpolation, Young absorption, and centering. All thirteen explicit binders of the statement are retained. The dimension premise and redundant majorant positivity premise are unused; an underscore prefix marks them and preserves their kinds, types and positions.

theorem HCPolySupport.HighContrast.Entry.fixed_geometry_positive_gap (d : ℕ) (_hd : 2 ≤ d) (N : ℝ) (hN : 2 ≤ N) (P : MeasureTheory.Measure (CoeffSpace d)) (hP : MeasureTheory.IsProbabilityMeasure P) (F G : CoeffSpace d → BlockMat d) (hF : SchattenMemLp P N F) (hG : SchattenMemLp P N G) (hFpos : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F a)) (_hGpos : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (G a)) (hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a)) : (lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (F a) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (F b) α β ∂P))) ≤ ((1 + (2 * ↑d) ^ N⁻¹) * lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (G b) α β ∂P))) + 2 * (1 + ↑d ^ (1 - N⁻¹)) * blockOpNorm (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (G b) α β ∂P)) ^ (1 - N⁻¹) * blockTrace (blockSub (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (G b) α β ∂P)) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (b : CoeffSpace d), blockMatEntry (F b) α β ∂P))) ^ N⁻¹

The printed positive-gap estimate with its exact coefficients.