Strictly preterminal positive-time bounds imply the full stopped integral bound

Proved

AvramDividend.Classical.lintegral_le_of_strict_terminal_positive_truncations

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

avram-dividendfinite-ruinmonotone-convergencepathwise-upperstopped-renewal

For a measurable stopped-payment region lying strictly before a finite positive terminal time T, if its restricted measure has no nonpositive-time mass and its discounted integrals through every finite cutoff t<T are bounded above by B, then its complete nonnegative integral is bounded by B. Rational cutoffs strictly between each payment time and T form a countable directed exhaustion, and monotone convergence supplies the full limit.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Add
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real

open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.lintegral_le_of_strict_terminal_positive_truncations
    (μ : Measure ℝ) (T : ℝ) (hT : 0 < T)
    (S : Set ℝ) (hS : MeasurableSet S)
    (hST : ∀ r ∈ S, r < T)
    (hzero : (μ.restrict S) (Set.Iic (0 : ℝ)) = 0)
    (f : ℝ → ℝ≥0∞) (hf : Measurable f) (B : ℝ≥0∞)
    (hbound : ∀ t : ℝ, 0 ≤ t → t < T →
      (∫⁻ r in S, if r ∈ Set.Ioc (0 : ℝ) t then f r else 0 ∂μ) ≤ B) :
    (∫⁻ r in S, f r ∂μ) ≤ B := by sorry

Source

Use rational density (exists_rat_btwn), directed monotone convergence for ℚ-subtype cutoffs, the restricted-measure support lemma and each preterminal truncated integral bound.

View graph