Exponential transform controls capped nonnegative Lévy drift-deficit increments

Proved

AvramDividend.Classical.nonnegative_truncated_le_exp_gap

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

avram-classicalcapped-incrementexp-estimateinfinite-activitymesh-bound

If 0≤x≤a with a>0, then x≤4a(1-exp(-x/(2a))). The inequality bounds the contribution of a capped increment to a finite-mesh Lévy deficit by its discounted Laplace deficit. It is an elementary scaling consequence of the proved exponential-deficit half-interval lemma.

Preamble

import Theorems.Thm_AvramDividend_Classical_exp_gap_dominates_half_interval
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

Formal statement

theorem AvramDividend.Classical.nonnegative_truncated_le_exp_gap
    (a x : ℝ) (ha : 0 < a) (hx0 : 0 ≤ x) (hxa : x ≤ a) :
    x ≤ 4 * a * (1 - Real.exp (-(x / (2 * a)))) := by sorry

Source

Proved exp_gap_dominates_half_interval, basic field algebra and positivity.

View graph