feat: x ^ n / n ! ≤ exp x (#9099)

Also make private/delete the intermediate lemmas of the form `x + 1 ≤ Real.exp x` so that people use the more general final results instead.

Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -52,14 +52,14 @@ theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp := by
     calc
       exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
       _ = exp y * (1 - exp (x - y)) := by ring
-      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp_of_nonzero h2.ne]
+      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
       _ = exp y * (y - x) := by ring
   · have h1 : 0 < z - y := by linarith
     rw [lt_div_iff h1]
     calc
       exp y * (z - y) < exp y * (exp (z - y) - 1) := by
         gcongr _ * ?_
-        linarith [add_one_lt_exp_of_nonzero h1.ne']
+        linarith [add_one_lt_exp h1.ne']
       _ = exp (z - y) * exp y - exp y := by ring
       _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
 #align strict_convex_on_exp strictConvexOn_exp

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -265,7 +265,7 @@ theorem log_lt_sub_one_of_pos (hx1 : 0 < x) (hx2 : x ≠ 1) : log x < x - 1 := b
   have h : log x ≠ 0
   · rwa [← log_one, log_injOn_pos.ne_iff hx1]
     exact mem_Ioi.mpr zero_lt_one
-  linarith [add_one_lt_exp_of_nonzero h, exp_log hx1]
+  linarith [add_one_lt_exp h, exp_log hx1]
 #align real.log_lt_sub_one_of_pos Real.log_lt_sub_one_of_pos
 
 theorem eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : log x = 0) : x = 1 :=

Mathlib/Combinatorics/Additive/Behrend.lean

@@ -340,8 +340,7 @@ theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x
   refine' le_trans _ (div_le_div_of_le_of_nonneg (exp_le_exp.2 h₂) <| add_nonneg hx.le zero_le_one)
   rw [le_div_iff (add_pos hx zero_lt_one), ← le_div_iff' (exp_pos _), ← exp_sub, neg_mul,
     sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]
-  refine' le_trans _ (add_one_le_exp_of_nonneg <| add_nonneg hx.le zero_le_one)
-  exact le_add_of_nonneg_right zero_le_one
+  exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)
 #align behrend.exp_neg_two_mul_le Behrend.exp_neg_two_mul_le
 
 theorem div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / exp 1) ≤ x) : x / exp 1 < (⌊x / 2⌋₊ : ℝ) := by

Mathlib/Data/Complex/Exponential.lean

@@ -1475,6 +1475,12 @@ theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i in range
     _ = exp x := by rw [exp, Complex.exp, ← cauSeqRe, lim_re]
 #align real.sum_le_exp_of_nonneg Real.sum_le_exp_of_nonneg
 
+lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=
+  calc
+    x ^ n / n ! ≤ ∑ k in range (n + 1), x ^ k / k ! :=
+        single_le_sum (f := fun k ↦ x ^ k / k !) (fun k _ ↦ by positivity) (self_mem_range_succ n)
+    _ ≤ exp x := sum_le_exp_of_nonneg hx _
+
 theorem quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2 ≤ exp x :=
   calc
     1 + x + x ^ 2 / 2 = ∑ i in range 3, x ^ i / i ! := by
@@ -1485,17 +1491,13 @@ theorem quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2
     _ ≤ exp x := sum_le_exp_of_nonneg hx 3
 #align real.quadratic_le_exp_of_nonneg Real.quadratic_le_exp_of_nonneg
 
-theorem add_one_lt_exp_of_pos {x : ℝ} (hx : 0 < x) : x + 1 < exp x :=
+private theorem add_one_lt_exp_of_pos {x : ℝ} (hx : 0 < x) : x + 1 < exp x :=
   (by nlinarith : x + 1 < 1 + x + x ^ 2 / 2).trans_le (quadratic_le_exp_of_nonneg hx.le)
-#align real.add_one_lt_exp_of_pos Real.add_one_lt_exp_of_pos
 
-/-- This is an intermediate result that is later replaced by `Real.add_one_le_exp`; use that lemma
-instead. -/
-theorem add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x := by
+private theorem add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x := by
   rcases eq_or_lt_of_le hx with (rfl | h)
   · simp
   exact (add_one_lt_exp_of_pos h).le
-#align real.add_one_le_exp_of_nonneg Real.add_one_le_exp_of_nonneg
 
 theorem one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x := by linarith [add_one_le_exp_of_nonneg hx]
 #align real.one_le_exp Real.one_le_exp
@@ -1506,11 +1508,16 @@ theorem exp_pos (x : ℝ) : 0 < exp x :=
     exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))
 #align real.exp_pos Real.exp_pos
 
+lemma exp_nonneg (x : ℝ) : 0 ≤ exp x := x.exp_pos.le
+
 @[simp]
 theorem abs_exp (x : ℝ) : |exp x| = exp x :=
   abs_of_pos (exp_pos _)
 #align real.abs_exp Real.abs_exp
 
+lemma exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x) := by
+  cases le_total x 0 <;> simp [abs_of_nonpos, _root_.abs_of_nonneg, exp_nonneg, *]
+
 @[mono]
 theorem exp_strictMono : StrictMono exp := fun x y h => by
   rw [← sub_add_cancel y x, Real.exp_add]
@@ -1970,48 +1977,42 @@ theorem exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1)
   · exact (exp_bound_div_one_sub_of_interval' h1 h2).le
 #align real.exp_bound_div_one_sub_of_interval Real.exp_bound_div_one_sub_of_interval
 
-theorem one_sub_lt_exp_minus_of_pos {y : ℝ} (h : 0 < y) : 1 - y < Real.exp (-y) := by
-  cases' le_or_lt 1 y with h' h'
-  · linarith [(-y).exp_pos]
-  rw [exp_neg, lt_inv _ y.exp_pos, inv_eq_one_div]
-  · exact exp_bound_div_one_sub_of_interval' h h'
-  · linarith
-#align real.one_sub_le_exp_minus_of_pos Real.one_sub_lt_exp_minus_of_pos
+theorem add_one_lt_exp {x : ℝ} (hx : x ≠ 0) : x + 1 < Real.exp x := by
+  obtain hx | hx := hx.symm.lt_or_lt
+  · exact add_one_lt_exp_of_pos hx
+  obtain h' | h' := le_or_lt 1 (-x)
+  · linarith [x.exp_pos]
+  have hx' : 0 < x + 1 := by linarith
+  simpa [add_comm, exp_neg, inv_lt_inv (exp_pos _) hx']
+    using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'
+#align real.add_one_lt_exp_of_nonzero Real.add_one_lt_exp
+#align real.add_one_lt_exp_of_pos Real.add_one_lt_exp
 
-theorem one_sub_le_exp_minus_of_nonneg {y : ℝ} (h : 0 ≤ y) : 1 - y ≤ Real.exp (-y) := by
-  rcases eq_or_lt_of_le h with (rfl | h)
+theorem add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x := by
+  obtain rfl | hx := eq_or_ne x 0
   · simp
-  · exact (one_sub_lt_exp_minus_of_pos h).le
-#align real.one_sub_le_exp_minus_of_nonneg Real.one_sub_le_exp_minus_of_nonneg
-
-theorem add_one_lt_exp_of_neg {x : ℝ} (h : x < 0) : x + 1 < Real.exp x := by
-  have h1 : 0 < -x := by linarith
-  simpa [add_comm] using one_sub_lt_exp_minus_of_pos h1
-#align real.add_one_lt_exp_of_neg Real.add_one_lt_exp_of_neg
+  · exact (add_one_lt_exp hx).le
+#align real.add_one_le_exp Real.add_one_le_exp
+#align real.add_one_le_exp_of_nonneg Real.add_one_le_exp
 
-theorem add_one_lt_exp_of_nonzero {x : ℝ} (hx : x ≠ 0) : x + 1 < Real.exp x := by
-  cases' lt_or_gt_of_ne hx with h h
-  · exact add_one_lt_exp_of_neg h
-  exact add_one_lt_exp_of_pos h
-#align real.add_one_lt_exp_of_nonzero Real.add_one_lt_exp_of_nonzero
+lemma one_sub_lt_exp_neg {x : ℝ} (hx : x ≠ 0) : 1 - x < exp (-x) :=
+  (sub_eq_neg_add _ _).trans_lt $ add_one_lt_exp $ neg_ne_zero.2 hx
 
-theorem add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x := by
-  cases' le_or_lt 0 x with h h
-  · exact Real.add_one_le_exp_of_nonneg h
-  exact (add_one_lt_exp_of_neg h).le
-#align real.add_one_le_exp Real.add_one_le_exp
+lemma one_sub_le_exp_neg (x : ℝ) : 1 - x ≤ exp (-x) :=
+  (sub_eq_neg_add _ _).trans_le $ add_one_le_exp _
+#align real.one_sub_le_exp_minus_of_pos Real.one_sub_le_exp_neg
+#align real.one_sub_le_exp_minus_of_nonneg Real.one_sub_le_exp_neg
 
 theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t / n) ^ n ≤ exp (-t) := by
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp
     rwa [Nat.cast_zero] at ht'
-  convert pow_le_pow_of_le_left ?_ (add_one_le_exp (-(t / n))) n using 2
-  · abel
+  convert pow_le_pow_of_le_left ?_ (one_sub_le_exp_neg (t / n)) n using 2
   · rw [← Real.exp_nat_mul]
     congr 1
     field_simp
     ring_nf
-  · rwa [add_comm, ← sub_eq_add_neg, sub_nonneg, div_le_one]
+  · rwa [sub_nonneg, div_le_one]
     positivity
 #align real.one_sub_div_pow_le_exp_neg Real.one_sub_div_pow_le_exp_neg