feat(Analysis/Complex/Exponential): add new bounds on exponential (leanprover-community#39690)

We add new upper bounds on Real.exp in terms of 2x/(2+x), and use these to move some bounds on log higher in mathlib.
We also add a lemma for the common bound (1+1/n)^n <= e, though this is a special-case of `one_sub_div_pow_le_exp_neg` (immediately before), but is added for convenience and discoverability, as this is a "well-known" bound.

Author: b-mehta

Mathlib/Analysis/Complex/Exponential.lean

@@ -11,6 +11,8 @@ public import Mathlib.Algebra.Order.CauSeq.BigOperators
 public import Mathlib.Algebra.Order.Star.Basic
 public import Mathlib.Data.Complex.BigOperators
 public import Mathlib.Data.Nat.Choose.Sum
+public import Mathlib.Tactic.NormNum.BigOperators
+public import Mathlib.Tactic.NormNum.NatFactorial
 
 /-!
 # Exponential Function
@@ -648,12 +650,35 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
       · exact one_sub_le_exp_neg _
     _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
 
+lemma one_add_inv_pow_le_exp {n : ℕ} : (1 + (n : ℝ)⁻¹) ^ n ≤ exp 1 := by
+  convert one_sub_div_pow_le_exp_neg (n := n) (t := -1) (by grind) using 1
+  · field
+  · simp
+
 lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := by
   rw [le_inv_mul_iff₀ hc]
   calc c * x
   _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
   _ ≤ _ := Real.add_one_le_exp (c * x)
 
+lemma exp_lt_two_add_div_two_sub {x : ℝ} (hx : 0 < x) (hx' : x < 2) :
+    exp x < (2 + x) / (2 - x) := by calc
+  _ = exp (x / 2) ^ 2 := by grind [Real.exp_nat_mul (x / 2) 2]
+  _ ≤ _ := by
+    grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)]
+    apply Real.exp_nonneg
+  _ < (2 + x) / (2 - x) := by
+    rw [lt_div_iff₀ (by linarith), ← sub_pos]
+    simp only [Finset.sum_range_succ]
+    ring_nf
+    positivity
+
+lemma exp_le_two_add_div_two_sub {x : ℝ} (hx : 0 ≤ x) (hx' : x < 2) :
+    exp x ≤ (2 + x) / (2 - x) := by
+  obtain rfl | hx₀ := hx.eq_or_lt
+  · simp
+  · exact (exp_lt_two_add_div_two_sub hx₀ hx').le
+
 theorem prod_one_add_le_exp_sum {ι : Type*} (s : Finset ι) {f : ι → ℝ}
     (hf : ∀ i, 0 ≤ f i) : ∏ i ∈ s, (1 + f i) ≤ exp (∑ i ∈ s, f i) :=
   (Finset.prod_le_prod (fun i _ ↦ add_nonneg zero_le_one (hf i))

Mathlib/Analysis/Complex/ExponentialBounds.lean

@@ -77,7 +77,7 @@ theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10 := by
   norm_num1 at z
   rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z
   apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
-  norm_num [sum_range_succ]
+  norm_num
 
 theorem log_two_gt_d9 : 0.6931471803 < log 2 :=
   lt_of_lt_of_le (by norm_num1) (sub_le_comm.1 (abs_sub_le_iff.1 log_two_near_10).2)

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -336,6 +336,16 @@ theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x|
   rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
   exact this
 
+lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by
+  rw [le_log_iff_exp_le (by grind)]
+  convert exp_le_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
+  all_goals field_simp; grind
+
+lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by
+  rw [lt_log_iff_exp_lt (by grind)]
+  convert exp_lt_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
+  all_goals field_simp; grind
+
 /-- The real logarithm function tends to `+∞` at `+∞`. -/
 theorem tendsto_log_atTop : Tendsto log atTop atTop :=
   tendsto_comp_exp_atTop.1 <| by simpa only [log_exp] using! tendsto_id

Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

@@ -423,14 +423,4 @@ theorem hasSum_log_one_add {a : ℝ} (h : 0 ≤ a) :
   · convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
     all_goals simp [field, add_comm]
 
-lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by
-  convert! le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1
-  simp [field]
-
-lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by
-  convert!
-    lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity) 1 (by positivity)
-      (by positivity) using 1
-  simp [field]
-
 end Real