MomentBoostedLargeAllP

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

All-exponent assembly for the moment-boosted large-cube route

This module joins the strict high-power carrier and the concave low-power carrier under one dimension-only envelope. Partition/window distinctions and the two exponent ranges are discharged here; the public result below this module has no such proof-engineering premises.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerWindowEnvelope (d : ℕ) : ℝ

Extra fixed window margin for the low-power branch.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeAllPConst (d : ℕ) : ℝ

The common dimension-only constant selected before the model, exponent, and scales.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeAllPConst_pos (d : ℕ) : 0 < momentBoostedLargeCubeAllPConst d

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

The head moment budget for a stream increment on a large cube.

Equations

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

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

The head moment budget with the spatial averaging decay factor.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeAllPTail M p l n m = Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeAllPHead M p n m * 3 ^ (-(↑d / 2) * (↑l - ↑m))

theorem Algsuperdiff.Section3.Provider.Stream.stream_increment_lp_large_cube_bound_provider (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (p : ℝ), 1 ≤ p → ∀ (l m n : ℤ), n < m → m ≤ l → Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) ((C * p) ^ (p / 2) * (min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m)) ^ (p / 2)) ((C * p) ^ (p / 2) * (min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m)) ^ (p / 2) * 3 ^ (-(↑d / 2) * (↑l - ↑m)))

The all-exponent provider behind the frozen large-cube source declaration. All range and partition cases are discharged internally; the sole displayed constant depends only on the dimension and is selected before the model and all scale parameters.