Closed-horizon shifted future survival equals rational relative-grid survival and a terminal test

Proved

AvramDividend.Classical.chat04_random_reserve_shifted_closed_survival_grid_iff

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

closed-horizongridkilled-semigroupshifted-incrementstwo-sided-exit

For arbitrary random reserve H(ω), deterministic clock shift b and relative horizon T, continuous survival H+X(b+v)-X(b)≥0 at every v≤T is equivalent to survival on all rational observations k/n strictly before T and one explicit terminal test at T. The theorem upgrades the strict shifted downcrossing grid equivalence and exactly bridges real future-window killing to the countable-grid Markov–Tonelli theorem for q-scale renewal.

Preamble

import Mathlib.Data.NNReal.Defs
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Theorems.Thm_AvramDividend_Classical_chat04_random_reserve_shifted_lower_before_horizon_grid_iff

open MeasureTheory
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_random_reserve_shifted_closed_survival_grid_iff
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (H : Ω → ℝ) (ω : Ω) (b T : ℝ≥0) :
    (∀ v : ℝ≥0, v ≤ T →
      0 ≤ H ω + (X.X (b + v) ω - X.X b ω)) ↔
    (∀ n : ℕ, 0 < n → ∀ k : ℕ,
      (k : ℝ≥0) * (n : ℝ≥0)⁻¹ < T →
        0 ≤ H ω +
          (X.X (b + (k : ℝ≥0) * (n : ℝ≥0)⁻¹) ω - X.X b ω)) ∧
    0 ≤ H ω + (X.X (b + T) ω - X.X b ω) := by sorry

Source

Proved chat04_random_reserve_shifted_lower_before_horizon_grid_iff and order dichotomy.

View graph