MomentBoostedKernel

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

Internal moment-boosted tail kernel for stream-increment masses

This module is internal probability infrastructure for the proof of e.kl.bounds.large (ABK26). It is not a source-facing replacement for that node and does not state a large-cube conclusion.

The usual conversion from Gamma_sigma moment growth to a weak-tail witness throws away the factor sigma⁻¹ available when the Markov exponent is chosen to be t^sigma. Retaining that factor gives the one-sided tail

exp (t^sigma / (2 sigma))⁻¹.

For sigma = 2 / p, its scale is a fixed base to the power p / 2, rather than the forbidden p^12 inflation from the generic Gamma_sigma triangle route. The later finite-range colored truncated-MGF argument consumes both the strengthened tail and the genuine centered second-moment estimate proved here.

No frozen declaration is imported.

References:

• ABK26 and Proposition p.concentration.

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

The strengthened one-sided tail naturally supplied by all-real Gamma_sigma moment growth. It is an internal kernel, not the source's Gamma_sigma tail function.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedGammaSigma sigma t = Real.exp (t ^ sigma / (2 * sigma))

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedGammaSigma_inv (sigma t : ℝ) : (momentBoostedGammaSigma sigma t)⁻¹ = Real.exp (-(t ^ sigma / (2 * sigma)))

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_of_momentBoostedGammaSigma {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {X : Omega → ℝ} {A sigma : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma ≤ 1) (h : HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) X A) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) X (4 * A)

A strengthened kernel tail controls the ordinary Gamma_sigma tail at a fixed factor-four enlargement whenever 0 < sigma ≤ 1. This conversion is used only for the bounded partition-window branch; the finite-family route retains the sharper kernel until after coloring.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_momentBoostedGammaSigma_of_momentGrowth {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {Y : Omega → ℝ} {M sigma : ℝ} (hsigma : 0 < sigma) (hM : 0 < M) (hY_nonneg : ∀ (omega : Omega), 0 ≤ Y omega) (hY : HCPolySupport.IndependentSums.HasGammaMomentGrowthWith mu sigma Y M) : HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) Y (2 ^ sigma⁻¹ * M)

All-real Gamma_sigma moment growth gives the strengthened one-sided tail at scale 2^(1/sigma) M.

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

The local scale for the later moment-boosted finite-range argument.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMomentBoostScale_pos {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : 0 < streamIncrementLpMomentBoostScale M p n m

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_centered_streamIncrementLpMass_momentBoosted {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (momentBoostedGammaSigma (2 / p)) (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => streamIncrementLpMass p l n m omega - ∫ (omega' : ℤ → Frozen.Assumptions.ShellField d), streamIncrementLpMass p l n m omega' ∂↑M.P) (streamIncrementLpMomentBoostScale M p n m)

The actual local stream-increment mass has the strengthened centered one-sided tail, uniformly in the observation scale l.

theorem Algsuperdiff.Section3.Provider.Stream.integrable_and_integral_centered_streamIncrementLpMass_sq_le {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => (streamIncrementLpMass p l n m omega - ∫ (omega' : ℤ → Frozen.Assumptions.ShellField d), streamIncrementLpMass p l n m omega' ∂↑M.P) ^ 2) ↑M.P ∧ ∫ (omega : ℤ → Frozen.Assumptions.ShellField d), (streamIncrementLpMass p l n m omega - ∫ (omega' : ℤ → Frozen.Assumptions.ShellField d), streamIncrementLpMass p l n m omega' ∂↑M.P) ^ 2 ∂↑M.P ≤ streamIncrementLpMomentBoostScale M p n m ^ 2

The same local mass has a genuine centered second-moment scale. This is the variance input to the finite-range truncated-MGF proof, not an extra premise of the source-facing large-cube statement.