Extended first-passage clocks coincide when all strict-horizon crossing witnesses coincide

Proved

AvramDividend.Classical.firstPassage_iInf_eq_of_strict_horizon_witness_iff

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

Two extended-real first-passage clocks defined as infima of possibly different families of candidate crossing times are equal if, for every extended horizon T, one family has a witness strictly before T exactly when the other has a witness strictly before T. This order-theoretic bridge connects countable-grid crossing-time detection to the continuous-time strict passage clocks in the renewal proof.

Preamble

import Mathlib.Data.ENNReal.Basic
import Mathlib.Order.CompleteLattice.Defs

open scoped ENNReal

Formal statement

theorem AvramDividend.Classical.firstPassage_iInf_eq_of_strict_horizon_witness_iff
    {ι κ : Sort*} (f : ι → ℝ≥0∞) (g : κ → ℝ≥0∞)
    (h : ∀ T : ℝ≥0∞, (∃ i, f i < T) ↔ (∃ j, g j < T)) :
    (⨅ i, f i) = (⨅ j, g j) := by sorry

Source

Mathlib.Order.CompleteLattice.Defs iInf_lt_iff and iInf_le. Supports using Proved chat03_upper_before_horizon_countable_grid_iff and its lower companion to identify countable full-path reward clocks with true Lévy passage clocks, for lower-bound UUID 6b821aa5-c792-4436-8eca-fc9429115ef9.

View graph