Stopped interval reward is bounded by the complete payment indicator integral

Proved

AvramDividend.Classical.stopped_interval_reward_le_full_indicator

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

For any measure on the real line and any measurable set of permitted payment times, the nonnegative exponentially discounted reward on the intersection with a time interval cannot exceed the full permitted payment reward. The result rewrites the restricted-measure integral as the full-space integral of its measurable indicator. It is the final measure-theoretic comparison needed to turn survived record-grid interval bounds into bounds against the genuine stopped dividend reward.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.Analysis.Complex.Exponential

open MeasureTheory Set
open scoped NNReal ENNReal Classical

Formal statement

theorem AvramDividend.Classical.stopped_interval_reward_le_full_indicator
    (μ : Measure ℝ) (S : Set ℝ) (hS : MeasurableSet S)
    (q a b : ℝ) :
    (∫⁻ t in S,
      if t ∈ Set.Ioc a b then
        ENNReal.ofReal (Real.exp (-(q * t))) else 0 ∂μ) ≤
    (∫⁻ t,
      if t ∈ S then ENNReal.ofReal (Real.exp (-(q * t))) else 0
      ∂μ) := by sorry

Source

Mathlib lintegral_mono and lintegral_indicator.

View graph