StreamIncrementLpLargeCube

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

theorem Algsuperdiff.Frozen.Section3.stream_increment_lp_large_cube_bound (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (p : ℝ), 1 ≤ p → ∀ (l m n : ℤ), n < m → m ≤ l → Section3.Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (Section3.Provider.Stream.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)))