Monotone first-record survival reduces killed budgets to surviving prefixes

Proved

AvramDividend.Classical.recordGrid_prefix_survival_weight_budget

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

Let record clocks T_n increase with n. If the undiscounted finite-prefix sum of nonnegative extended-real record rewards is bounded by C whenever the Nth clock precedes the stopping horizon, then every killed finite-prefix sum is bounded by C, including paths where ruin interrupts the grid. The proof splits at the last summand and inducts on the prefix length, using monotone clocks to remove the survival indicators when the final crossing survives.

Preamble

import Mathlib.Data.ENNReal.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

open scoped NNReal ENNReal BigOperators

Formal statement

theorem AvramDividend.Classical.recordGrid_prefix_survival_weight_budget
    (T : ℕ → ℝ≥0∞) (hT : Monotone T)
    (τ : ℝ≥0∞) (f : ℕ → ℝ≥0∞) (C : ℝ≥0∞)
    (hprefix : ∀ N : ℕ, T N < τ →
      (∑ n ∈ Finset.range N, f n) ≤ C) :
    ∀ N : ℕ,
      (∑ n ∈ Finset.range N,
        if T (n + 1) < τ then f n else 0) ≤ C := by sorry

Source

Finset.sum_range_succ, Finset.sum_congr, monotone clock survival and elementary Nat order.

View graph