Polynomial bounds on the real exponential

Two Taylor-type bounds on the real exponential for nonnegative arguments. They are the scalar inequalities behind multiplicative Chernoff bounds and the Johnson–Lindenstrauss lemma.

• exp (-x) ≤ 1 - x + x² / 2 (Real.exp_neg_le_one_sub_add_sq_div_two): multiply by exp x ≥ 1 + x + x² / 2.
• 1 + x ≤ exp (x - x² / 2 + x³ / 3) (Real.one_add_le_exp_sub_sq_div_two_add_cube_div_three), equivalently log (1 + x) ≤ x - x² / 2 + x³ / 3. The exponent v is nonnegative. The degree-four Taylor polynomial 1 + v + v² / 2 + v³ / 6 + v⁴ / 24 is at most exp v and already dominates 1 + x, by an explicit sum of nonnegative terms.

CslibFrontier.Foundations.Analysis.SpecialFunctions.ExpLogQuadratic has the weaker Real.exp_neg_le_one_sub_add_sq, exp (-y) ≤ 1 - y + y², valid for all -1 ≤ y.

Main results

• Real.exp_neg_le_one_sub_add_sq_div_two: exp (-x) ≤ 1 - x + x² / 2 for 0 ≤ x.
• Real.one_add_le_exp_sub_sq_div_two_add_cube_div_three: 1 + x ≤ exp (x - x² / 2 + x³ / 3) for 0 ≤ x.
• Real.exp_neg_two_le_one_third: exp (-2) ≤ 1 / 3.
• Real.two_pow_le_exp: 2 ^ n ≤ exp n.
• Real.one_sub_pow_le_exp: (1 - p) ^ R ≤ exp (-c) for p ≤ 1 and c ≤ R p.
• Real.pow_le_one_third: p ^ k ≤ 1 / 3 for 0 ≤ p ≤ 1 - δ and 2 ≤ δ k.

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

exp (-x) ≤ 1 - x + x² / 2 for 0 ≤ x.

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

1 + x ≤ exp (x - x² / 2 + x³ / 3) for 0 ≤ x; equivalently log (1 + x) ≤ x - x² / 2 + x³ / 3.

theorem Real.exp_neg_two_le_one_third : exp (-2) ≤ 1 / 3

exp (-2) ≤ 1 / 3.

theorem Real.two_pow_le_exp (n : ℕ) : 2 ^ n ≤ exp ↑n

2 ^ n ≤ exp n, since 2 ≤ exp 1.

theorem Real.one_sub_pow_le_exp {p c : ℝ} {R : ℕ} (hp1 : p ≤ 1) (hc : c ≤ ↑R * p) : (1 - p) ^ R ≤ exp (-c)

(1 - p) ^ R ≤ exp (-c) once c ≤ R p.

theorem Real.pow_le_one_third {p δ : ℝ} {k : ℕ} (hp : 0 ≤ p) (hpδ : p ≤ 1 - δ) (hk : 2 ≤ δ * ↑k) : p ^ k ≤ 1 / 3

Amplification bound: if 0 ≤ p ≤ 1 - δ and 2 ≤ δ k, then p ^ k ≤ 1 / 3.