Bounded exponential gap of a nonnegative random variable is integrable under a finite measure

Proved

AvramDividend.Classical.nonnegative_exp_deficit_integrable

by WillR · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicalexponentialfinite-meshintegrabilitynonnegative-deficit

For an almost surely nonnegative real random variable on a finite measure space and a nonnegative parameter theta, the exponential deficit 1-exp(-theta*D) lies between zero and one almost everywhere. If that deficit is almost-everywhere strongly measurable, it is integrable by Integrable.of_bound. This is the integrability needed for the exponential mesh-gap moment of the bounded-variation Lévy drift deficit.

Preamble

import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Tactic.Linarith

open MeasureTheory

Formal statement

theorem AvramDividend.Classical.nonnegative_exp_deficit_integrable
    {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P]
    (D : Ω → ℝ) (θ : ℝ) (hθ : 0 ≤ θ)
    (hNonneg : ∀ᵐ ω ∂P, 0 ≤ D ω)
    (hMeas : AEStronglyMeasurable
      (fun ω => (1 : ℝ) - Real.exp (-θ * D ω)) P) :
    Integrable (fun ω => (1 : ℝ) - Real.exp (-θ * D ω)) P := by sorry

Source

Mathlib Integrable.of_bound and Real.exp_le_one_iff.

View graph