UpperFiniteQLtTwoAggregation

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

Section 3.3 finite-exponent upper aggregation below two

This module passes from a normalized, per-descendant three-term block split to the finite-q < 2 upper coarse-ellipticity payload. The only caller-supplied analytic input is the per-descendant split. The pointwise summability demanded by the existing finite-q consumer is recovered here from its per-depth weak-Orlicz bounds by changing the normalized depth families on a measurable null set.

The deterministic ordinary and rare scale-series estimates are discharged internally before the resulting split is packaged in the upper-tail carrier.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperFiniteQLtTwoRareBudgetConst (d : ℕ) : ℝ

The strengthened rare normalizer shared with the other two upper-exponent branches. The second triangle factor is needed by the q ≥ 2 fold and is harmless in the present q < 2 branch.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upper_finite_lt_two_of_per_descendant {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (r : { r : ℝ // 1 ≤ r }) (hr : ↑r < 2) {sigma s scaling Cblock eps Cup : ℝ} (hsigma0 : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hs : 0 < s) (hs1 : s ≤ 1) (hscaling : 0 ≤ scaling) (hCblock : 0 < Cblock) (heps : 0 < eps) (heps1 : eps ≤ 1) (hwin : M.gamma / 2 + eps ≤ s) (hCup : 0 < Cup) (hdetHead : 4 * Cblock ≤ Cup) (hordinaryHead : 147456 * HCPolySupport.IndependentSums.gammaTriangleConst 1 * gridNetConst d 1 * Cblock ≤ Cup) (hper : ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∃ (Uone : Cutoff.CutoffSample d → ℝ) (Uexp : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ Uone omega) ∧ Measurable Uone ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ Uexp omega) ∧ Measurable Uexp ∧ (∀ (omega : Cutoff.CutoffSample d), cutoffBBlockFamily M m scaling R omega ≤ Cblock + Uone omega + Uexp omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) Uone (upperSaturatedPerCubeAmplitude Cblock (Disorder.cstar M) M.gamma k) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) Uexp ((upperFiniteQLtTwoRareBudgetConst d)⁻¹ * 3 ^ (M.gamma * (↑k + 1)) * eps ^ 15)) : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s hs (CoarseEllipticityExponent.finite r) omega * scaling) Cup (Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) eps

The finite-q < 2 upper carrier from the normalized per-descendant split. All deterministic scale summability and budget obligations are discharged in this theorem; the caller supplies only the normalized block split and the two dimension-only merge inequalities.