Uniform Esscher exponential downcrossing probability bound on an entire countable bounded monotone time schedule

Proved

AvramDividend.Classical.chat04_esscher_positive_root_countable_monotone_grid_downcrossing_probability_bound

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

countable-griddoobesscherlevy-processes

Let g:ℕ→ℝ≥0 be any bounded monotone observation schedule with g(k)≤T. Under the genuine terminal φ-Esscher probability law, for q>0 and positive root ψφ=q, the bound exp(φb/2)·Q_T(∃k:X_{g(k)}≤−b)≤1 holds for the entire countably infinite observation schedule. This is obtained without any infinite-horizon tilted law, by finite-grid Doob bounds uniform in the prefix length and measure continuity from below.

Preamble

import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.Probability.Process.Filtration
import Mathlib.Analysis.Complex.Exponential
import Theorems.Thm_AvramDividend_Classical_chat04_esscher_positive_root_finite_grid_downcrossing_probability_bound
import Theorems.Thm_AvramDividend_Classical_uniform_weighted_finite_prefix_measure_bound_extends_to_countable_union
open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_esscher_positive_root_countable_monotone_grid_downcrossing_probability_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q φ b : ℝ) (hq : 0 < q) (hφ : 0 < φ)
    (hroot : X.ψ φ = q)
    (T : ℝ≥0) (g : ℕ → ℝ≥0) (hg : Monotone g)
    (hgT : ∀ k : ℕ, g k ≤ T)
    (a : ℝ≥0) (ha : (a : ℝ) = Real.exp ((φ / 2) * b)) :
    (a : ℝ≥0∞) *
      (P.withDensity (fun ω : Ω => ENNReal.ofReal
        (Real.exp (φ * X.X T ω - (T : ℝ) * X.ψ φ))))
        {ω : Ω | ∃ k : ℕ, X.X (g k) ω ≤ -b} ≤ 1 := by sorry

Source

Define measurable nested prefix events s_n={∃k≤n:X(g k)≤−b}. Show monotonicity and measurability using adaptedness of the Lévy process, the filtration's ambient inclusion and countable union of preimages of Ici/Iic. Use accepted `chat04_esscher_positive_root_finite_grid_downcrossing_probability_bound` for every n and accepted `uniform_weighted_finite_prefix_measure_bound_extends_to_countable_union` for the full union, identified with the countable downcrossing event by straightforward set extensionality.

View graph