UpperFiniteQGeTwoInfinityAggregation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Upper aggregation for finite exponents at least two and infinity #
This module aggregates a strict-descendant per-cube decomposition through the
joint grid-and-depth ordinary envelope and the normalized rare folded pole. Its
public theorem supplies both the finite-q ≥ 2 and q = ∞ upper Orlicz
bounds from the same per-descendant estimate.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.upper_finite_two_le_and_infinity_of_per_descendant
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
(M : ABKModel d)
(m : ℤ)
{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)
(hgamma1 : M.gamma ≤ 1)
(hgap : 0 < 2 * s - M.gamma)
(hwin : M.gamma / 2 + eps ≤ s)
(hCup : 0 < Cup)
(hCblockCup : Cblock ≤ Cup)
(hordinaryHead : 1152 * triadicJointDepthEntropyConst d * 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
((4 * upperAfterBandRareTriangleConst ^ 2 * 1658880 ^ 2 * upperAfterBandRareGridNetConst d)⁻¹ * 3 ^ (M.gamma * (↑k + 1)) * eps ^ 15))
:
(∀ (r : { r : ℝ // 1 ≤ r }),
2 ≤ ↑r →
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) ∧ ∀ (q : CoarseEllipticityExponent),
↑q = HCPolySupport.Book.Ch02.MultiscaleExponent.infinity →
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 q omega * scaling) Cup
(Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) eps
Aggregate one per-descendant ordinary/rare decomposition simultaneously
for every finite exponent q ≥ 2 and for the infinite exponent.