MomentBoostedLargeProvider

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

Internal wrapper for the strict p > 2 large-partition branch

This module packages the fully discharged sharp branch in the exact one-sided-Orlicz shape used by the frozen large-cube theorem. Its additional partition-window and strict-exponent conditions are internal case-split data; they are discharged by the final all-p assembly and do not appear in the source-facing export.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeTargetScale {d : ℕ} (M : ABKModel d) (p : ℝ) (l n m : ℤ) : ℝ

The target scale combining the large-cube moment budget and spatial decay.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.isDeterministicShiftOneSidedOrlicz_streamIncrementLpMass_p_gt_two_partition {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : 2 < p) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) : Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) (streamIncrementLpMassHead M p n m) (momentBoostedLargeCubeTargetScale M p l n m)

The genuinely sharp p > 2 partition branch, already in the exact one-sided wrapper shape. hsl is an internal partition normalization condition, not a source premise.

theorem Algsuperdiff.Section3.Provider.Stream.isDeterministicShiftOneSidedOrlicz_streamIncrementLpMass_p_gt_two {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : 2 < p) {n m l : ℤ} (hnm : n < m) (hml : m ≤ l) : Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) (streamIncrementLpMassHead M p n m) (momentBoostedLargeCubeTargetScale M p l n m)

The strict-exponent branch with the manuscript's m ≤ l source window. Both internal partition regimes are discharged here.