SubgaussianTail #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Gaussian tails give square integrability #
The paper's J2 tail bound is a literal strict upper-tail estimate. This module
turns that estimate, with no added moment hypothesis, into the L² input
needed to construct the stationary J4 observable.
theorem
Algsuperdiff.Probability.memLp_two_of_gaussian_tail
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → ℝ}
(hXmeas : Measurable X)
(hXnonneg : ∀ (ω : Ω), 0 ≤ X ω)
(htail : ∀ (t : ℝ), 1 ≤ t → μ {ω : Ω | t < X ω} ≤ ENNReal.ofReal (Real.exp (-t ^ 2)))
:
MeasureTheory.MemLp X 2 μ
A nonnegative measurable real random variable with the paper's strict
Gaussian upper tail (above level one) belongs to L².