A zero initial atom lets open-right reward windows dominate closed-left prefixes

Proved

AvramDividend.Classical.lintegral_Ico_le_Ioc_of_zero_initial_atom

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

For any nonnegative Stieltjes reward density and measure with no atom at zero, its integral over [0,t) is at most its integral over (0,t]. The set [0,t) lies in (0,t] union {0}; use monotonicity and subadditivity of set integrals and the null singleton. Needed to combine rational-prefix exhaustion with finite-horizon dividend estimates.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic

open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.lintegral_Ico_le_Ioc_of_zero_initial_atom
    (μ : Measure ℝ) (f : ℝ → ℝ≥0∞) (t : ℝ)
    (hzero : μ ({0} : Set ℝ) = 0) :
    (∫⁻ r in Ico (0 : ℝ) t, f r ∂μ) ≤
      (∫⁻ r in Ioc (0 : ℝ) t, f r ∂μ) := by sorry

Source

Use lintegral_mono_set for [0,t) subset (0,t] union {0}, lintegral_union_le, and setLIntegral_measure_zero.

View graph