BoundsEaLProviderFinal

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

bounds_mathcal_E_aL: the unconditional provider-final

What this module delivers

MinkowskiProviderFinal.bounds_mathcal_E_aL_provider_of_perCubeMoments reduces the anchor to ONE per-cube L^{p/2}-moment obligation hcube at the three-shape majorant minkowskiScaleMajorant. This module discharges it:

1. PerCubeSixWay.lintegral_rpow_lFreeStep3Majorant_le_of_summands splits the L-free Step-3 majorant into its three named summands at the absolute cost 2 (the negated leg, priced by the proved negation invariance of the law);
2. each summand is bounded at the anchor's own slots -- the FIRST and THIRD at K p γ s^{-2} (PerCubeSlotFirst, PerCubeSlotThird), the SECOND at K p (γ(m−j) + γ) 3^{2γ(m−j)} (PerCubeSlotSecond);
3. the anchor's own window (γ ≤ C^{-10}, s ∈ [C²√γ, 1/4], p ≤ C^{-1}γ^{-1}s) supplies the four scalar facts the slot bounds need: γ ≤ 1/8, 8γ ≤ s, 1 ≤ p/2 and 8(p/2) ≤ γ^{-1}. NOTHING else about p is used: the anchor's printed range stands unchanged.

References

• ABK26, l.bounds.mathcal.E.aL, Steps 1--5.

1. The per-cube obligation, discharged

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_perCubeMoments (d : ℕ) [NeZero d] (cstar : ℝ) (hcstar : 0 < cstar) (Cd : ℝ) (hCd : 0 < Cd) : ∃ (K : ℝ), 0 < K ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ K⁻¹ ^ 10 → ∀ (m n : ℤ), n ≤ m → ↑m ≤ ↑n + M.gamma⁻¹ → ∀ s ∈ Set.Icc (K ^ 2 * √M.gamma) (1 / 4), ∀ p ∈ Set.Icc (2 * ↑d * s⁻¹) (K⁻¹ * M.gamma⁻¹ * s), ∀ (l : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (n - ↑l), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (lFreeStep3Majorant Cd M m s (lFreeGradSlot m (tailSeriesGauge m)) (lFreeValueSlot m (tailSeriesGauge m)) R omega) ^ (p / 2) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (minkowskiScaleMajorant K p M.gamma s (↑m - ↑n) l) ^ (p / 2)

hcube, discharged.

For every positive Step-3 display constant there is a constant K such that, in the anchor's own window, the p/2-th moment of the L-free Step-3 majorant at every descendant cube is at most the three-shape majorant minkowskiScaleMajorant K p γ s (m−n) l raised to the p/2.

This is Step 5's inner (Hölder) half, in full.

2. The provider-final

theorem Algsuperdiff.Section4.Provider.BoundsEaL.bounds_mathcal_E_aL_provider (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ C⁻¹ ^ 10 → ∀ (m n : ℤ), n ≤ m → ↑m ≤ ↑n + M.gamma⁻¹ → ∀ s ∈ Set.Icc (C ^ 2 * √M.gamma) (1 / 4), ∀ (hs : 0 < s), ∀ p ∈ Set.Icc (2 * ↑d * s⁻¹) (C⁻¹ * M.gamma⁻¹ * s), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m n ⟨s, hs⟩ omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * Real.rpow 3 (1 / 2 * s * (↑m - ↑n)) * √p * (s⁻¹ + √(↑m - ↑n)) * √M.gamma) ^ p

The provider-final, unconditional.