A uniform exponential-deficit bound for nonnegative arguments at most one half

Proved

AvramDividend.Classical.exp_gap_dominates_half_interval

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

avram-classicalbounded-variationexp-estimateinfinite-activitypath-regularity

For 0≤u≤1/2, u is bounded by twice the exponential deficit 1-exp(-u). This elementary deterministic estimate is used in controlling expected capped Lévy drift-deficit increments from their exact Laplace moments in the bounded-variation infinite-activity no-local-monotonicity argument.

Preamble

import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

Formal statement

theorem AvramDividend.Classical.exp_gap_dominates_half_interval
    (u : ℝ) (hu : 0 ≤ u) (hhalf : u ≤ (1 / 2 : ℝ)) :
    u ≤ 2 * (1 - Real.exp (-u)) := by sorry

Source

Real.add_one_le_exp and the identity exp(u)exp(-u)=1 in pinned Mathlib.

View graph