SecondTermSlots #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 5's second summand: the slots it reads, and their moments #

What this module supplies #

The S summand of MajorantSlots.step3DisplayAt is the one Step 5 handles "with additional inputs". Before its p/2-moment can be written down, three slot facts are needed that the proved layer does not yet carry:

the two-term ℝ≥0∞ Minkowski step in the development normal form (lintegral_rpow_real_add_le_of_moments), for a SUM of two real observables;
the L-free VALUE slot's own moment, i.e. bullet (B6b) with its two legs -- the L∞ leg of ValueSlotLinfty and the mean-value tail of ValueSlotMoment -- summed (lintegral_rpow_lFreeValueSlot_le).
the a.e. measurability of the three named summands of step3DisplayAt separately, which is what PerCubeSixWay's six-way split asks for at the untouched sample.

Everything here is either a proved bullet read at a new exponent or generic measure theory; no γ-power, no s-power and no parameter range is moved.

References #

ABK26, l.bounds.mathcal.E.aL, bullet (B6b), Step 5.

1. Two-term Minkowski in the development normal form #

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_real_add_le_of_moments {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {F G : Omega → ℝ} {RF RG q : ℝ} (hq : 1 ≤ q) (hFm : AEMeasurable F mu) (hGm : AEMeasurable G mu) (hRF : 0 ≤ RF) (hRG : 0 ≤ RG) (hF : ∫⁻ (omega : Omega), ENNReal.ofReal (F omega) ^ q ∂mu ≤ ENNReal.ofReal RF ^ q) (hG : ∫⁻ (omega : Omega), ENNReal.ofReal (G omega) ^ q ∂mu ≤ ENNReal.ofReal RG ^ q) :

∫⁻ (omega : Omega), ENNReal.ofReal (F omega + G omega) ^ q ∂mu ≤ ENNReal.ofReal (RF + RG) ^ q

The two-term Minkowski step observables, in the development normal form ∫⁻ (ofReal ·)^q ≤ (ofReal R)^q.

2. The `L`-free value slot: nonnegativity, measurability, moment #

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lFreeValueSlot_tailSeriesGauge_nonneg {d : ℕ} (m : ℤ) (R : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) :

0 ≤ lFreeValueSlot m (tailSeriesGauge m) R omega

The L-free value slot is nonnegative at the canonical tail gauge.

source

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.valueSlotMajorant {d : ℕ} (M : Section3.ABKModel d) (m j : ℤ) (r : ℝ) :

ℝ

The value slot's majorant at moment r: the two legs of bullet (B6b), summed.

Equations

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

Instances For

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.valueSlotMajorant_nonneg {d : ℕ} (M : Section3.ABKModel d) (m j : ℤ) (r : ℝ) :

0 ≤ valueSlotMajorant M m j r

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_lFreeValueSlot_le {d : ℕ} (M : Section3.ABKModel d) {m : ℤ} (R : HCPolySupport.TriadicCube d) (hjm : R.scale ≤ m) {r : ℝ} (hr : 1 ≤ r) :

∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (lFreeValueSlot m (tailSeriesGauge m) R omega) ^ r ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (valueSlotMajorant M m R.scale r) ^ r

Bullet (B6b), both legs, at every moment r ∈ [1,∞).

The L-free value slot is the sum of the L∞ leg and the mean-value tail, so ℝ≥0∞ Minkowski gives its moment as the sum of the two proved ones. This is the form Step 5's second summand consumes.