High-contrast homogenization: Entry.Analysis.PositiveGap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
PositiveGap random-field assembly #
This module assembles the ordered random difference and the deterministic mean-gap
receipts that the positive-gap estimates consume, and proves the nonlinear, Young
absorption and centered forms of the positive-gap estimate l.fixed.geometry.positive.gap.
theorem
HCPolySupport.HighContrast.Analysis.positiveGap_ordered_data
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsFiniteMeasure P]
{N : ℝ}
(hN : 1 ≤ N)
{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))
(hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a))
:
have D := fun (a : CoeffSpace d) => blockSub (G a) (F a);
have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P);
have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P);
SchattenMemLp P N D ∧ (∀ᵐ (a : CoeffSpace d) ∂P, Matrix.PosSemidef (toFullBlockMat (D a)) ∧ BlockMatLoewnerLE (D a) (G a)) ∧ ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (D a) α β ∂P) = blockSub MG MF ∧ Matrix.PosSemidef (toFullBlockMat MF) ∧ Matrix.PosSemidef (toFullBlockMat MG) ∧ Matrix.PosSemidef (toFullBlockMat (blockSub MG MF)) ∧ BlockMatLoewnerLE (blockSub MG MF) MG
The ordered difference D = G - F and its entrywise mean receipts.
theorem
HCPolySupport.HighContrast.Analysis.positiveGap_mean_gap_bounds
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsFiniteMeasure P]
{N : ℝ}
(hN : 1 ≤ N)
{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))
(hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a))
:
have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P);
have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P);
0 ≤ blockTrace (blockSub MG MF) ∧ absSchattenNorm N (blockSub MG MF) ≤ blockTrace (blockSub MG MF) ∧ blockTrace (blockSub MG MF) ≤ 2 * ↑d * blockOpNorm MG ∧ blockTrace (blockSub MG MF) ≤ (2 * ↑d) ^ (1 - N⁻¹) * blockOpNorm MG ^ (1 - N⁻¹) * blockTrace (blockSub MG MF) ^ N⁻¹
Deterministic mean-gap bounds used in the centering step.
theorem
HCPolySupport.HighContrast.Analysis.positiveGap_nonlinear
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{N : ℝ}
(hN : 1 < N)
{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))
(hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a))
:
have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P);
have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P);
(lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) (F a)) ≤ blockOpNorm MG ^ (1 - N⁻¹) * blockTrace (blockSub MG MF) ^ N⁻¹ + (2 * ↑d) ^ ((N - 1) / N ^ 2) * (lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) MG) ^ (1 - N⁻¹) * (lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) (F a)) ^ N⁻¹
l.fixed.geometry.positive.gap: the nonlinear inequality, with genuine scalar moments and
finite real norm readbacks. The Hölder inputs are the centered majorant and gap
Schatten functions, with conjugate exponents N/(N-1) and N.
theorem
HCPolySupport.HighContrast.Analysis.positiveGap_young_absorption
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{N : ℝ}
(hN : 1 < N)
{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))
(hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a))
:
have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P);
have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P);
(lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) (F a)) ≤ ((2 * ↑d) ^ N⁻¹ * lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) MG) + N / (N - 1) * blockOpNorm MG ^ (1 - N⁻¹) * blockTrace (blockSub MG MF) ^ N⁻¹
l.fixed.geometry.positive.gap: Young absorption of the proved nonlinear estimate,
with the printed dimension and rational coefficients.
theorem
HCPolySupport.HighContrast.Analysis.positiveGap_centered_bound
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{N : ℝ}
(hN : 1 < N)
{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))
(hFG : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (G a))
:
have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P);
have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P);
(lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (F a) MF) ≤ ((1 + (2 * ↑d) ^ N⁻¹) * lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (G a) MG) + (N / (N - 1) + (2 * ↑d) ^ (1 - N⁻¹)) * blockOpNorm MG ^ (1 - N⁻¹) * blockTrace (blockSub MG MF) ^ N⁻¹
l.fixed.geometry.positive.gap: center using two sharp subtraction inequalities,
then bound the deterministic mean gap and insert Young absorption.