MomentBoostedIndependentEndpoint

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

Internal sharp independent-family endpoint for moment-boosted tails

This file is a deterministic probability lemma used internally by the large-cube proof. Starting with a one-sided tail whose exponent retains the factor sigma⁻¹, it optimizes the truncated-MGF estimate of MomentBoostedChernoff.lean for one independent finite family. Its constant is a fixed numerical base raised only to 1 / sigma; it therefore does not introduce the forbidden p^12 loss when sigma = 2 / p.

It is not a source-facing stream statement. Finite-range coloring and the actual stream variables are supplied separately.

Reference: ABK26, Proposition p.concentration.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentVariance (sigma : ℝ) : ℝ

A deliberately generous, fixed numerical variance envelope.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentVariance sigma = 4 * 8192 ^ (2 / sigma)

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentVariance_pos {sigma : ℝ} : 0 < momentBoostedIndependentVariance sigma

theorem Algsuperdiff.Section3.Provider.Stream.sqrt_momentBoostedIndependentVariance {sigma : ℝ} (hsigma : 0 < sigma) : √(momentBoostedIndependentVariance sigma) = 2 * 8192 ^ (1 / sigma)

theorem Algsuperdiff.Section3.Provider.Stream.two_le_sqrt_momentBoostedIndependentVariance {sigma : ℝ} (hsigma : 0 < sigma) : 2 ≤ √(momentBoostedIndependentVariance sigma)

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentVariance_dominates {sigma : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma < 1) : 1 / 2 + Real.exp 1 / 2 + 48 ^ (2 / sigma) / 2 ≤ momentBoostedIndependentVariance sigma

The MGF quadratic coefficient is bounded by the fixed variance envelope.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentTilt (sigma D R t : ℝ) : ℝ

The cutoff which balances the MGF tilt against the strengthened tail.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentTilt sigma D R t = t ^ (sigma - 1) / (4 * √D * √R)

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentCutoff (sigma D R t : ℝ) : ℝ

The truncation cutoff associated with the independent moment-boosted tilt.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedIndependentCutoff sigma D R t = (√D * √R / sigma) ^ (1 / (1 - sigma)) * t

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_finset_sum_momentBoosted_independent {Omega : Type u_1} {iota : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : iota → Omega → ℝ} {s : Finset iota} {sigma : ℝ} (hs : s.Nonempty) (h_indep : ProbabilityTheory.iIndepFun X mu) (h_meas : ∀ (i : iota), Measurable (X i)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) mu) (h_sq : ∀ i ∈ s, MeasureTheory.Integrable (fun (omega : Omega) => |X i omega| ^ 2) mu) (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) (X i) 1) (hmean : ∀ i ∈ s, ∫ (omega : Omega), X i omega ∂mu = 0) (hsecond : ∀ i ∈ s, ∫ (omega : Omega), |X i omega| ^ 2 ∂mu ≤ 1) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Omega) => ∑ i ∈ s, X i omega) (16 * √(momentBoostedIndependentVariance sigma) * √↑s.card)

A sharp one-sided Gamma_sigma tail for an independent centered finite family at its true square-root cardinality scale.