feat(Analysis/Complex/ExponentialBounds): round e = 3 (leanprover-community#33440)

Also adds `2 < e < 3` and `e⁻¹ < 1/2` that might be more easily applicable than the stronger approximations.

Author: SnirBroshi

Mathlib/Analysis/Complex/ExponentialBounds.lean

@@ -37,6 +37,23 @@ theorem exp_one_gt_d9 : 2.7182818283 < exp 1 :=
 theorem exp_one_lt_d9 : exp 1 < 2.7182818286 :=
   lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) (by norm_num)
 
+theorem exp_one_gt_two : 2 < exp 1 :=
+  lt_trans (by norm_num) exp_one_gt_d9
+
+theorem exp_one_lt_three : exp 1 < 3 :=
+  lt_trans exp_one_lt_d9 (by norm_num)
+
+theorem floor_exp_one_eq_two : ⌊exp 1⌋ = 2 :=
+  Int.floor_eq_iff.mpr ⟨exp_one_gt_two.le, by exact_mod_cast exp_one_lt_three⟩
+
+theorem ceil_exp_one_eq_three : ⌈exp 1⌉ = 3 :=
+  Int.ceil_eq_iff.mpr ⟨by exact_mod_cast exp_one_gt_two, exp_one_lt_three.le⟩
+
+theorem round_exp_one_eq_three : round (exp 1) = 3 := by
+  refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨?_, by grind [exp_one_lt_three]⟩
+  grw [← exp_one_gt_d9]
+  norm_num
+
 theorem exp_neg_one_gt_d9 : 0.36787944116 < exp (-1) := by
   rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]
   · refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_
@@ -47,6 +64,9 @@ theorem exp_neg_one_lt_d9 : exp (-1) < 0.3678794412 := by
   rw [exp_neg, inv_lt_comm₀ (exp_pos _) (by norm_num)]
   exact lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)
 
+theorem exp_neg_one_lt_half : exp (-1) < 1 / 2 :=
+  lt_trans exp_neg_one_lt_d9 (by norm_num)
+
 theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10 := by
   suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34) by
     norm_num1 at *

Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

@@ -293,7 +293,7 @@ theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) 
     _ ≤ log (2 ^ 3) * (69 / 50) := by
       gcongr
       · field_simp
-        simp (disch := positivity) [show 2 < Real.exp 1 from lt_trans (by norm_num1) exp_one_gt_d9]
+        simp (disch := positivity) [exp_one_gt_two]
       · norm_num1
         exact two_div_one_sub_two_div_e_le_eight
     _ ≤ √(log (2 ^ 12)) := by
@@ -319,7 +319,7 @@ theorem div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / exp 1) ≤ x) : x / exp 1 < (
   apply lt_of_le_of_lt _ (sub_one_lt_floor _)
   have : 0 < 1 - 2 / exp 1 := by
     rw [sub_pos, div_lt_one (exp_pos _)]
-    exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
+    exact exp_one_gt_two
   rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
     div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff₀ this]
   · exact zero_lt_two
@@ -414,7 +414,7 @@ theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dV
     exact hN.trans_lt' (by norm_num1)
   · refine div_pos zero_lt_two ?_
     rw [sub_pos, div_lt_one (exp_pos _)]
-    exact lt_of_le_of_lt (by norm_num1) exp_one_gt_d9
+    exact exp_one_gt_two
   positivity
 
 theorem roth_lower_bound_explicit (hN : 4096 ≤ N) :