High-contrast homogenization: Provider.Quenched.SmallContrastWeakEnergyTail

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

The bad-event optimizer energy under the source envelope

The bad-event optimizer energy of the weak-norm split, at the inflated reference 2·boundaryConst·3^{gG}·E, is bounded through the parametric bad-energy estimate: the excess part (M − 1/2)⁺ of the maximal function is supported on the source tail and has fourth moments decaying like 3^{-2Δ} by the crude-moment display, with Δ = t + G − 1 − s_K the gap between the generation scale and the growth witness. No window multiplier and no history enters.

noncomputable def HCPolySupport.HighContrast.Quenched.sourceMomentSix (K : ℝ) : ℝ

The crude-moment constant of order six.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Quenched.badMomentMajorant (K : ℝ) (Delta : ℤ) : ℝ

The decayed fourth-moment majorant of the maximal excess.

Equations

• HCPolySupport.HighContrast.Quenched.badMomentMajorant K Delta = 3 ^ (-(2 * ↑Delta)) * HCPolySupport.HighContrast.Quenched.sourceMomentSix K / 16

theorem HCPolySupport.HighContrast.Quenched.sourceMomentSix_nonneg (K : ℝ) : 0 ≤ sourceMomentSix K

theorem HCPolySupport.HighContrast.Quenched.badMomentMajorant_nonneg (K : ℝ) (Delta : ℤ) : 0 ≤ badMomentMajorant K Delta

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_four_le_of_lintegral_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {W : CoeffSpace d → ENNReal} {h : ℝ} (hh : 0 ≤ h) (hmom : ∫⁻ (a : CoeffSpace d), W a ^ 4 ∂P ≤ ENNReal.ofReal h) (hW : AEMeasurable W P) : MeasureTheory.eLpNorm W (ENNReal.ofReal 4) P ≤ ENNReal.ofReal (h ^ 4⁻¹)

The L⁴ norm of a nonnegative extended statistic through its fourth moment.

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_const_four {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (c : ENNReal) : MeasureTheory.eLpNorm (fun (x : CoeffSpace d) => c) (ENNReal.ofReal 4) P = c

The L⁴ norm of an extended constant on a probability space.