MomentBoostedTruncation

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

Internal truncated-MGF kernel for strengthened moment tails

This file starts the analytic p > 2 branch needed internally by the exact e.kl.bounds.large provider. It does not state a source-facing stream bound. The first lemma keeps the sigma⁻¹ in the strengthened tail from MomentBoostedKernel, which is what prevents the generic heavy-tail A's exponential-in-sigma⁻² loss.

No declaration, import, or code path from that repository is used.

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

Half of the strengthened tail exponent.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedKernelCoeff sigma = 1 / (4 * sigma)

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedKernelCoeff_pos {sigma : ℝ} (hsigma : 0 < sigma) : 0 < momentBoostedKernelCoeff sigma

theorem Algsuperdiff.Section3.Provider.Stream.momentBoosted_tail_kernel_pointwise {sigma l L t : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hl : 0 ≤ l) (hlL : l ≤ momentBoostedKernelCoeff sigma * L ^ (sigma - 1)) (ht : t ∈ Set.Icc 1 L) : (2 * t + l * t ^ 2) * Real.exp (l * t) * Real.exp (-(t ^ sigma / (2 * sigma))) ≤ (2 * t + momentBoostedKernelCoeff sigma * t ^ (sigma + 1)) * Real.exp (-(momentBoostedKernelCoeff sigma * t ^ sigma))

A positive MGF tilt below the cutoff is absorbed by the strengthened one-sided moment tail.

theorem Algsuperdiff.Section3.Provider.Stream.momentBoosted_tail_integrand_pointwise_of_isBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {X : Omega → ℝ} {sigma l L t : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hX : HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) X 1) (hl : 0 ≤ l) (hlL : l ≤ momentBoostedKernelCoeff sigma * L ^ (sigma - 1)) (ht : t ∈ Set.Icc 1 L) : (2 * t + l * t ^ 2) * Real.exp (l * t) * mu.real {omega : Omega | t < X omega} ≤ (2 * t + momentBoostedKernelCoeff sigma * t ^ (sigma + 1)) * Real.exp (-(momentBoostedKernelCoeff sigma * t ^ sigma))

The analytic kernel also controls the actual upper-tail integrand of an observable with strengthened moment tail at unit scale.

theorem Algsuperdiff.Section3.Provider.Stream.mgf_upperTruncation_le_exp_of_secondMoment_and_tail {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} {l L C2 K : ℝ} (hXm : Measurable X) (hXint : MeasureTheory.Integrable X mu) (hXsq : MeasureTheory.Integrable (fun (omega : Omega) => |X omega| ^ 2) mu) (hXmean : ∫ (omega : Omega), X omega ∂mu = 0) (hsecond : ∫ (omega : Omega), |X omega| ^ 2 ∂mu ≤ C2) (hl : 0 ≤ l) (hl1 : l ≤ 1) (hL : 1 ≤ L) (hlarge : ∫ (t : ℝ) in Set.Ioc 1 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * mu.real {omega : Omega | t ≤ X omega} ≤ K) : ProbabilityTheory.mgf (HCPolySupport.IndependentSums.upperTruncation X L) mu l ≤ Real.exp (l ^ 2 * (C2 / 2 + Real.exp 1 / 2 + K / 2))

An internal one-variable truncated-MGF reduction. The second-moment and large-tail inputs are kept separate so that the moment-boosted kernel may provide the latter without invoking the generic Gamma_sigma triangle constant.

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

The deterministic integral envelope generated by the boosted tail. It is an internal analytic constant, not a stream-level estimate.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedTailKernelConst_le_fixedBase {sigma : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma < 1) : momentBoostedTailKernelConst sigma ≤ 48 ^ (2 / sigma)

The boosted tail kernel has a fixed-base envelope. Crucially, the coefficient 1 / (4 sigma) cancels the sigma⁻¹ in the Gamma integral before the elementary exponential factors are estimated.

theorem Algsuperdiff.Section3.Provider.Stream.integral_Ioc_one_L_tail_le_momentBoosted_fixedBase {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} {sigma l L : ℝ} (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hX : HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) X 1) (hl : 0 ≤ l) (hL : 1 ≤ L) (hlL : l ≤ momentBoostedKernelCoeff sigma * L ^ (sigma - 1)) : ∫ (t : ℝ) in Set.Ioc 1 L, (2 * t + l * t ^ 2) * Real.exp (l * t) * mu.real {omega : Omega | t ≤ X omega} ≤ 48 ^ (2 / sigma)

The strengthened upper tail supplies the large-interval input to the truncated-MGF estimate with a fixed base, uniformly in sigma ∈ (0,1).