Vanishing expected nonnegative deficit on an event and zero atomlessness force that event to be null

Proved

AvramDividend.Classical.zero_integral_positive_deficit_event_null

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

avram-classicalinfinite-activityintegral-zeronull-eventzero-barrier

Let D be an almost surely nonnegative random variable that is nonzero almost surely. If the expectation of D restricted to an arbitrary event E vanishes and the indicated random variable is integrable, then E has probability zero. This converts the bounded-variation Levy finite-mesh expected survival-deficit limit into a genuine zero-reflected-survival null event, avoiding any need for integrability of large negative jumps outside the survival event.

Preamble

import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.OuterMeasure.AE
import Mathlib.MeasureTheory.Measure.Restrict

open MeasureTheory Set

Formal statement

theorem AvramDividend.Classical.zero_integral_positive_deficit_event_null
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (P : Measure Ω) (E : Set Ω) (D : Ω → ℝ)
    (hD : ∀ᵐ ω ∂P, 0 ≤ D ω)
    (hAtom : P {ω : Ω | D ω = 0} = 0)
    (hIntegrable : Integrable (E.indicator D) P)
    (hIntegral : (∫ ω, E.indicator D ω ∂P) = 0) :
    P E = 0 := by sorry

Source

Mathlib integral_eq_zero_iff_of_nonneg_ae, Set.indicator_of_mem, MeasureTheory.ae_iff.

View graph