feat(data/complex): numerical bounds on log 2 (#7146)

Upper and lower bounds on log 2. Presumably these could be made faster but I don't know the tricks - the proof of `log_two_near_10` (for me) doesn't take longer than `exp_one_near_20` to compile.

I also strengthened the existing bounds slightly.

src/data/complex/exponential_bounds.lean

@@ -5,6 +5,9 @@ Authors: Mario Carneiro, Joseph Myers
 -/
 
 import data.complex.exponential
+import analysis.special_functions.exp_log
+import algebra.continued_fractions.computation.approximation_corollaries
+
 /-!
 # Bounds on specific values of the exponential
 -/
@@ -31,24 +34,48 @@ begin
   rw [_root_.abs_one, abs_of_pos]; norm_num1,
 end
 
-lemma exp_one_gt_271828182 : 2.71828182 < exp 1 :=
+lemma exp_one_gt_d9 : 2.7182818283 < exp 1 :=
 lt_of_lt_of_le (by norm_num) (sub_le.1 (abs_sub_le_iff.1 exp_one_near_10).2)
 
-lemma exp_one_lt_271828183 : exp 1 < 2.71828183 :=
+lemma 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)
 
-lemma exp_neg_one_gt_0367879441 : 0.367879441 < exp (-1) :=
+lemma exp_neg_one_gt_d9 : 0.36787944116 < exp (-1) :=
 begin
   rw [exp_neg, lt_inv _ (exp_pos _)],
   refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) _,
   all_goals {norm_num},
 end
 
-lemma exp_neg_one_lt_0367879442 : exp (-1) < 0.367879442 :=
+lemma exp_neg_one_lt_d9 : exp (-1) < 0.36787944120 :=
 begin
   rw [exp_neg, inv_lt (exp_pos _)],
   refine lt_of_lt_of_le _ (sub_le.1 (abs_sub_le_iff.1 exp_one_near_10).2),
   all_goals {norm_num},
 end
 
+lemma log_two_near_10 : abs' (log 2 - 287209 / 414355) ≤ 1/10^10 :=
+begin
+  suffices : abs' (log 2 - 287209 / 414355) ≤ 1/17179869184 + (1/10^10 - 1/2^34),
+  { norm_num1 at *,
+    assumption },
+  have t : abs' (2⁻¹ : ℝ) = 2⁻¹,
+  { rw abs_of_pos, norm_num },
+  have z := real.abs_log_sub_add_sum_range_le (show abs' (2⁻¹ : ℝ) < 1, by { rw t, norm_num }) 34,
+  rw t at z,
+  norm_num1 at z,
+  rw [one_div (2:ℝ), log_inv, ←sub_eq_add_neg, _root_.abs_sub] at z,
+  apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _),
+  simp_rw [sum_range_succ],
+  norm_num,
+  rw abs_of_pos;
+  norm_num
+end
+
+lemma log_two_gt_d9 : 0.6931471803 < log 2 :=
+lt_of_lt_of_le (by norm_num1) (sub_le.1 (abs_sub_le_iff.1 log_two_near_10).2)
+
+lemma log_two_lt_d9 : log 2 < 0.6931471808 :=
+lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 log_two_near_10).1) (by norm_num)
+
 end real