Integrability of a nonnegative drift deficit bounded on a survival event under a finite measure

Proved

AvramDividend.Classical.bounded_survival_deficit_indicator_integrable

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

avram-classicalfinite-meshintegrabilitysurvival-eventzero-barrier

Even if the unrestricted BV Lévy drift deficit has infinite expectation due to large downward jumps, its indicator restricted to the strict zero-barrier survival event is bounded by physical drift times the survival horizon. On any finite measure space, almost-sure nonnegativity, this eventwise upper bound, and almost-sure strong measurability imply its Bochner integrability. This discharges a critical assumption in the accepted finite-mesh expected-survival bound.

Preamble

import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith

open MeasureTheory Set

Formal statement

theorem AvramDividend.Classical.bounded_survival_deficit_indicator_integrable
    {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P]
    (E : Set Ω) (D : Ω → ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hMeas : AEStronglyMeasurable (E.indicator D) P)
    (hNonneg : ∀ᵐ ω ∂P, 0 ≤ D ω)
    (hBound : ∀ ω ∈ E, D ω ≤ C) :
    Integrable (E.indicator D) P := by sorry

Source

Mathlib Integrable.of_bound and real norm simplification.

View graph