Quadratic upper bounds for the real exponential

Mathlib records the lower bound 1 + x + x ^ 2 / 2 ≤ exp x for 0 ≤ x (Real.quadratic_le_exp_of_nonneg). This file supplies the matching upper bounds:

• Real.exp_le_one_add_add_sq_div_two_of_nonpos: for x ≤ 0, exp x ≤ 1 + x + x ^ 2 / 2;
• Real.exp_le_one_add_add_sq_div_of_le: if x ≤ c with 0 ≤ c < 3, then exp x ≤ 1 + x + x ^ 2 / (2 * (1 - c / 3)).

The second bound is the exponential estimate behind Bernstein's inequality: applied to t X for a centred random variable X ≤ b it bounds the moment-generating function by the second moment.

In the other direction, the lower bound gives Real.neg_mul_abs_sub_sq_div_le_mul_add_mul_exp_div: for V > 0, -S |t| - S ^ 2 / V ≤ t S + V exp (2 t) / 2. This controls the part of a Liouville-type energy ∫ (K u + e^(2u) / 2) dV carried by the mean t of u, with S = ∫ K dV and V the volume (TauCeti.Manifold.exists_le_liouvilleEnergy_add).

References

• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press (2013), §2.8.

theorem Real.exp_le_one_add_add_sq_div_two_of_nonpos {x : ℝ} (hx : x ≤ 0) : exp x ≤ 1 + x + x ^ 2 / 2

For x ≤ 0, the exponential lies below its second-order Taylor polynomial at 0.

theorem Real.exp_le_one_add_add_sq_div_of_le {x c : ℝ} (hxc : x ≤ c) (hc0 : 0 ≤ c) (hc3 : c < 3) : exp x ≤ 1 + x + x ^ 2 / (2 * (1 - c / 3))

Bernstein's exponential bound. If x ≤ c with 0 ≤ c < 3, then exp x ≤ 1 + x + x ^ 2 / (2 * (1 - c / 3)). Only an upper bound on x is needed: negative x are covered by Real.exp_le_one_add_add_sq_div_two_of_nonpos.

theorem Real.neg_mul_abs_sub_sq_div_le_mul_add_mul_exp_div {S V t : ℝ} (hV : 0 < V) : -S * |t| - S ^ 2 / V ≤ t * S + V * exp (2 * t) / 2

Real numbers S, t and V > 0 satisfy t S + V exp (2 t) / 2 ≥ -S |t| - S ^ 2 / V. For t ≥ 0 this follows from exp (2 t) ≥ 1 + 2 t + 2 t ^ 2 and (V t + S) ^ 2 ≥ 0.