Surviving finite record-prefix rewards are bounded by the killed infinite grid sum

Proved

AvramDividend.Classical.surviving_record_prefix_budget_le_killed_tsum

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

avram-dividendennreal-tsumfinite-gridpathwise-upperstopped-renewal

For any monotone extended record clocks c, their finite real representatives u through index N, and a stopping horizon after record N, the sum of N+1 initial-record discounted h-payments is at most the countable sum of killed record payments. Each finite-prefix term survives the stopping test, matches its actual extended clock, and the finite prefix is dominated by the ENNReal infinite sum. This supplies the final pathwise algebraic step from finite-horizon Stieltjes cell budgets to the killed renewal weights used in the original upper-bound theorem.

Preamble

import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
import Mathlib.Analysis.Complex.Exponential
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic

open scoped NNReal ENNReal BigOperators Classical

Formal statement

theorem AvramDividend.Classical.surviving_record_prefix_budget_le_killed_tsum (τ : ℝ≥0∞) (q h : ℝ) (hh : 0 ≤ h)
    (c : ℕ → ℝ≥0∞) (u : ℕ → ℝ≥0) (N : ℕ)
    (hc : ∀ k : ℕ, k ≤ N → c k = (u k : ℝ≥0∞))
    (hmono : ∀ k : ℕ, k ≤ N → c k ≤ c N)
    (hSurvive : (u N : ℝ≥0∞) < τ) :
    (∑ k ∈ Finset.range (N + 1),
      ENNReal.ofReal (Real.exp (-(q * (u k : ℝ)))) *
        ENNReal.ofReal h) ≤
    (∑' k : ℕ,
      if c k < τ then
        ENNReal.ofReal
          (h * Real.exp (-(q * (c k).toReal)))
      else 0) := by sorry

Source

Use equality of finite record clocks with their NNReal representatives, monotone survival through index N, ENNReal.ofReal_mul, and ENNReal.tsum_eq_iSup_nat.

View graph