High-contrast homogenization: Provider.Entry.SourceMoment

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

The source moment of the random-source data

The comparison between adapted and Euclidean cubes measures its error in units of the reference block with the source gauge Γ_{g,S}(j) = (1-g)^{-1}(1 + K_{Ψ_S}^2 3^{-j})^g as coefficient, and the one place the law of the source scale enters its proof is the moment of the source scale,

E[S] ≤ 2K_{Ψ_S}^2.

This file proves it, and the integrability of the source scale that comes with it, from the random-source data alone.

Iterating the gauge growth of e.source.tail twice against Ψ_S ≥ 1 gives Ψ_S(σ) ≥ σ^2K_{Ψ_S}^{-3} for σ ≥ K_{Ψ_S}^2, so the tail is quadratic there. The layer-cake integral of the tail then splits at K_{Ψ_S}^2: below it the tail is bounded by one and contributes the length K_{Ψ_S}^2, above it the quadratic tail integrates to K_{Ψ_S}, and K_{Ψ_S} ≤ K_{Ψ_S}^2 since the witness exceeds one.

There are no definitions in this file.

The source moment

theorem HCPolySupport.HighContrast.Entry.sq_div_le_gauge {Ψ : ℝ → ℝ} {K : ℝ} (hK : 1 < K) (hadm : IndependentSums.AdmissiblePsi Ψ) (hgrow : IndependentSums.HasPsiGrowth Ψ K) {σ : ℝ} (hσ : K ^ 2 ≤ σ) : σ ^ 2 / K ^ 3 ≤ Ψ σ

The gauge is at least quadratic above the square of its witness. Iterating the growth inequality of e.source.tail twice, at the arguments σK_{Ψ_S}^{-2} and σK_{Ψ_S}^{-1}, and using Ψ_S ≥ 1.

theorem HCPolySupport.HighContrast.Entry.measureReal_tail_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {σ : ℝ} (hσ : K ^ 2 ≤ σ) : P.real {a : CoeffSpace d | σ < S a} ≤ K ^ 3 * σ ^ (-2)

The quadratic tail of the source scale above the square of the gauge witness, from e.source.tail and the quadratic lower bound on the gauge.

theorem HCPolySupport.HighContrast.Entry.lintegral_source_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (S a) ∂P ≤ ENNReal.ofReal (K ^ 2 + K)

The layer-cake bound behind the source moment: the split of ∫_0^∞ P[S > σ]dσ at K_{Ψ_S}^2.

theorem HCPolySupport.HighContrast.Entry.integrable_source {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : MeasureTheory.Integrable S P

The source scale is integrable: its quadratic tail is.

theorem HCPolySupport.HighContrast.Entry.integral_source_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : ∫ (a : CoeffSpace d), S a ∂P ≤ 2 * K ^ 2

The source moment: E[S] ≤ 2K_{Ψ_S}^2.