PthMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Moment integration for the displacement tail #
This module isolates the integration step behind ABK26
e.pth.moment.process. A normalized exponential tail gives the displayed
p^p moment dependence with the explicit constant 6.
theorem
Algsuperdiff.Section5.Provider.integral_rpow_le_of_exp_tail
{Omega : Type u_1}
[MeasurableSpace Omega]
(mu : MeasureTheory.Measure Omega)
[MeasureTheory.IsProbabilityMeasure mu]
{W : Omega → ℝ}
(hW : AEMeasurable W mu)
(hWnn : 0 ≤ᵐ[mu] W)
(htail : ∀ (s : ℝ), 0 < s → mu.real {omega : Omega | s < W omega} ≤ 2 * Real.exp (-s))
{p : ℝ}
(hp : 1 ≤ p)
:
A nonnegative random variable with tail at most 2 exp (-s) has moments
bounded by (6p)^p, for every real exponent p >= 1.