Every finite horizon has no first record or a final attained grid record

Proved

AvramDividend.Classical.record_grid_last_survived_before_finite_horizon

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

avram-dividendfinite-horizonfirst-passagepathwise-upperrecord-grid

Fix a positive record spacing and any finite observation horizon T, independently of whether dividend ruin is finite or infinite. Either the first positive record threshold has not been crossed strictly before T, or some last grid threshold b+n h is crossed strictly before T while the next threshold is not. A finite-horizon path is bounded above, so sufficiently high record clocks lie beyond T; the conclusion then follows by induction on the grid index. This supplies a finite truncation for global stopped-renewal upper estimates.

Preamble

import Mathlib.Data.Nat.Basic
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_record_grid_clocks_eventually_ge_horizon

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.record_grid_last_survived_before_finite_horizon
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω)
    (b h : ℝ) (hh : 0 < h) (T : ℝ≥0) :
    (¬ (⨅ (r : ℝ≥0) (_ : b < X.X r ω), (r : ℝ≥0∞)) <
      (T : ℝ≥0∞)) ∨
    ∃ n : ℕ,
      (⨅ (r : ℝ≥0)
        (_ : b + (n : ℝ) * h < X.X r ω), (r : ℝ≥0∞)) <
        (T : ℝ≥0∞) ∧
      ¬ (⨅ (r : ℝ≥0)
        (_ : b + ((n + 1 : ℕ) : ℝ) * h < X.X r ω), (r : ℝ≥0∞)) <
        (T : ℝ≥0∞) := by sorry

Source

Direct consequence of the accepted eventual finite-horizon record-clock bound, with finite induction to select the final strict pre-horizon crossing.

View graph