Extended-real exponential threshold exactly identifies downward crossing

Proved

AvramDividend.Classical.ennreal_exp_downcrossing_threshold_iff

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

exponentialorder-theoryruin-probability

For ε>0, b,y real, the inequality ENNReal.ofReal(exp(ε b))≤ENNReal.ofReal(exp(−ε y)) is equivalent to y≤−b. This is the precise event identification needed to convert an Esscher-exponential Markov estimate into a lower-crossing probability bound, including boundary equality.

Preamble

import Mathlib.Data.ENNReal.Real
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Algebra.Order.Field.Basic
open scoped ENNReal

Formal statement

theorem AvramDividend.Classical.ennreal_exp_downcrossing_threshold_iff
    (ε b y : ℝ) (hε : 0 < ε) :
    (ENNReal.ofReal (Real.exp (ε * b)) ≤
      ENNReal.ofReal (Real.exp (-ε * y))) ↔ y ≤ -b := by sorry

Source

Use the pinned ENNReal.ofReal_le_ofReal_iff on positive exponential images, the strict real exponential order equivalence and positivity of ε to cancel the positive multiplier. No Lévy-specific hypotheses are required.

View graph