A right-persistent upper crossing has an inverse-natural grid witness before every horizon

Proved

AvramDividend.Classical.rightInterval_upper_before_horizon_grid_iff

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

Any nonnegative-time real-valued path whose strict upper crossings persist for some right interval has a crossing before horizon T exactly when it has a positive-denominator rational-grid crossing before T. This deterministic result applies to shifted paths of Lévy processes as well as their original trajectories.

Preamble

import Mathlib.Data.NNReal.Defs
import Theorems.Thm_AvramDividend_Classical_chat03_nnreal_grid_ceiling_bracket

open scoped NNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.rightInterval_upper_before_horizon_grid_iff
    (g : ℝ≥0 → ℝ) (upper : ℝ)
    (hRight : ∀ s : ℝ≥0, upper < g s →
      ∃ u : ℝ≥0, s < u ∧
        ∀ r : ℝ≥0, s ≤ r → r < u → upper < g r)
    (T : ℝ≥0) :
    (∃ s : ℝ≥0, s < T ∧ upper < g s) ↔
    ∃ n : ℕ, 0 < n ∧ ∃ k : ℕ,
      (k : ℝ≥0) * (n : ℝ≥0)⁻¹ < T ∧
        upper < g ((k : ℝ≥0) * (n : ℝ≥0)⁻¹) := by sorry

Source

Generalises the Proved chat03_upper_before_horizon_countable_grid_iff by isolating its sole right-interval hypothesis; uses Proved NNReal grid-ceiling bracket and the pinned inverse-natural Archimedean lemma.

View graph