Auxiliary layer-cake identities for Doob's L² maximal inequality.
Reference: O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2002.
theorem
BGW.Probability.lintegral_sq_eq_tail
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → ℝ}
(hf : Measurable f)
(hnn : ∀ (ω : Ω), 0 ≤ f ω)
:
The tail-integral formula for the square of a nonnegative measurable function.
theorem
BGW.Probability.lintegral_tail_eq
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite μ]
{f g : Ω → ℝ}
(hf : Measurable f)
(hg : Measurable g)
:
Tonelli's theorem applied to the integral of g over the tail sets of f.
theorem
BGW.Probability.lintegral_sq_le_two_mul_of_tail
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite μ]
{f g : Ω → ℝ}
(hf : Measurable f)
(hg : Measurable g)
(hfnn : ∀ (ω : Ω), 0 ≤ f ω)
(htail :
∀ (t : ℝ), 0 < t → ENNReal.ofReal t * μ {ω : Ω | t ≤ f ω} ≤ ∫⁻ (ω : Ω) in {ω : Ω | t ≤ f ω}, ENNReal.ofReal (g ω) ∂μ)
:
∫⁻ (ω : Ω), ENNReal.ofReal (f ω) ^ 2 ∂μ ≤ 2 * ∫⁻ (ω : Ω), ENNReal.ofReal (f ω) * ENNReal.ofReal (g ω) ∂μ
A tail estimate t μ(f ≥ t) ≤ ∫_{f ≥ t} g for t > 0 implies ∫ f² ≤ 2 ∫ f g.