Strict ruin in a shifted Lévy future window is detected by a rational relative-time grid

Proved

AvramDividend.Classical.chat04_random_reserve_shifted_lower_before_horizon_grid_iff

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

killed-semigrouprational-gridshifted-incrementsstrict-ruintwo-sided-exit

For any deterministic Lévy splitting time b, arbitrary random reserve H(ω), finite relative horizon T, and sample path ω, strict negative reserve at any relative time before T occurs if and only if it occurs at some countable inverse-natural relative mesh k/n strictly before T. The proof uses shifted strict-crossing right-interval persistence and a ceiling-grid bracket. This identifies the true future-window killing event with the countable-grid event used in the Proved killed-scale Markov–Tonelli factorisation, upstream of two_sided_exit_stopped_scale_identity.

Preamble

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

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

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

Source

Proved shifted random-reserve strict right interval lemma and chat03_nnreal_grid_ceiling_bracket.

View graph