MinkowskiProviderFinal

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

bounds_mathcal_E_aL: the provider-final at the corrected ordering

What this module delivers

Composing

• MinkowskiScaleClosure.minkowskiScaleSum_total_le and sqrt_minkowskiScaleSum_le (the three per-scale shapes evaluated and rooted),
• SigmaBarLandmark.exists_pos_forall_model_of_two_le_dimension (the 2 ≤ d binder removal, which is what lets the provider match the anchor's binder order ∃ C before ∀ M),

gives the anchor's frozen block from a single per-cube L^{p/2}-moment obligation in the named shape minkowskiScaleMajorant.

The remaining obligation

hcube is the ONLY hypothesis beyond the anchor's own binders. It asks, for every positive Step-3 display constant, for a constant K such that the p/2-th moment of the L-free Step-3 majorant at a descendant cube of scale n − l is at most

K p ( γ s^{-2} + γ((m−n)+l) 3^{2γ((m−n)+l)} + γ 3^{2γ((m−n)+l)} )

raised to the p/2. The obligation is stated at an arbitrary display constant because step3DisplayAt is linear in that constant and every proved per-cube moment is already stated at an arbitrary one.

References

• ABK26, l.bounds.mathcal.E.aL, Step 5.

1. The per-scale majorant of the obligation

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.minkowskiScaleMajorant (K p gam s D : ℝ) (l : ℕ) : ℝ

The three per-scale shapes, named. K p γ (s^{-2} + (D+l)3^{2γ(D+l)} + 3^{2γ(D+l)}), with D = m − n and l the descendant depth below n.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.minkowskiScaleMajorant_nonneg {K p gam s D : ℝ} (hK : 0 ≤ K) (hp : 0 ≤ p) (hgam : 0 ≤ gam) (hD : 0 ≤ D) (l : ℕ) : 0 ≤ minkowskiScaleMajorant K p gam s D l

theorem Algsuperdiff.Section4.Provider.BoundsEaL.tsum_ofReal_scaleMajorant_le {K p gam s D : ℝ} (hK : 0 ≤ K) (hp : 0 ≤ p) (hs : 0 < s) (hs1 : s ≤ 1) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hD : 0 ≤ D) (hgamD : gam * D ≤ 1) : ∑' (l : ℕ), ENNReal.ofReal (HCPolySupport.Book.Ch02.geometricDiscount s 2 * (Real.rpow 3 (-s * ↑l) * minkowskiScaleMajorant K p gam s D l)) ≤ ENNReal.ofReal (K * p * (gam * (2 * (s⁻¹ * s⁻¹) + 36 * D + 180 / s)))

The transport's scale sum, closed at the named majorant (in ℝ≥0∞).

2. The provider-final

theorem Algsuperdiff.Section4.Provider.BoundsEaL.bounds_mathcal_E_aL_provider_of_perCubeMoments (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) (hcube : 2 ≤ d → ∀ (Cd : ℝ), 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)) : ∃ (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, at the corrected ordering.

Everything outside hcube is proved here: the 2 ≤ d binder removal, the window arithmetic (γ ≤ 1/8, 4γ ≤ s, γ(m−n) ≤ 1 -- all from the anchor's own γ ≤ C^{-10}, s ≥ C²√γ and m ≤ n + γ^{-1}), the Minkowski-ordered transport, the three-shape scale sum, and the square root against the anchor's printed scalar.