log_10_in_interval

proof body

Tactic-mode proof.

 370  simp only [contains, log10Interval]
 371  -- log(10) = log(2 * 5) = log(2) + log(5)
 372  -- log(5) = log(4 * 1.25) = log(4) + log(1.25) = 2*log(2) + log(1.25)
 373  -- So log(10) = log(2) + 2*log(2) + log(1.25) = 3*log(2) + log(1.25)
 374  have h_log10_eq : log 10 = 3 * log 2 + log (5/4) := by
 375    have h1 : (10 : ℝ) = 8 * (5/4) := by norm_num
 376    have h2 : (8 : ℝ) = 2^(3 : ℕ) := by norm_num
 377    calc log 10 = log (8 * (5/4)) := by rw [h1]
 378      _ = log 8 + log (5/4) := Real.log_mul (by norm_num) (by norm_num)
 379      _ = log (2^(3 : ℕ)) + log (5/4) := by rw [h2]
 380      _ = (3 : ℕ) * log 2 + log (5/4) := by rw [Real.log_pow]
 381      _ = 3 * log 2 + log (5/4) := by norm_num
 382  -- Bounds on log(2) from Mathlib
 383  have h_log2_gt : log 2 > 0.6931471803 := Real.log_two_gt_d9
 384  have h_log2_lt : log 2 < 0.6931471808 := Real.log_two_lt_d9
 385  -- Bounds on log(5/4) = log(1.25) using Taylor series
 386  -- log(1 + x) for x = 0.25: 0.25 - 0.25²/2 + 0.25³/3 - ... ≈ 0.2231
 387  have h_log125_gt : log (5/4) > 0.223 := by
 388    -- log(1.25) > 0.223 ↔ exp(0.223) < 1.25
 389    rw [gt_iff_lt, Real.lt_log_iff_exp_lt (by norm_num : (0 : ℝ) < 5/4)]
 390    -- exp(0.223) < 1.25
 391    have hx_abs : |(0.223 : ℝ)| ≤ 1 := by norm_num
 392    have h_bound := Real.exp_bound hx_abs (n := 5) (by norm_num : 0 < 5)
 393    have h_upper := (abs_sub_le_iff.mp h_bound).1
 394    have h_taylor : (∑ m ∈ Finset.range 5, (0.223 : ℝ)^m / m.factorial) +
 395        |(0.223 : ℝ)|^5 * (6 : ℕ) / (Nat.factorial 5 * 5) < 1.25 := by
 396      simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
 397                 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.223)]
 398      norm_num
 399    linarith
 400  have h_log125_lt : log (5/4) < 0.224 := by
 401    -- log(1.25) < 0.224 ↔ 1.25 < exp(0.224)
 402    rw [Real.log_lt_iff_lt_exp (by norm_num : (0 : ℝ) < 5/4)]
 403    -- exp(0.224) > 1.25
 404    have hx_abs : |(0.224 : ℝ)| ≤ 1 := by norm_num
 405    have h_bound := Real.exp_bound hx_abs (n := 4) (by norm_num : 0 < 4)
 406    have h_lower := (abs_sub_le_iff.mp h_bound).2
 407    have h_sum : (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
 408        |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) > 1.25 := by
 409      simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
 410                 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.224)]
 411      norm_num
 412    calc (5/4 : ℝ) = 1.25 := by norm_num
 413      _ < (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
 414          |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) := h_sum
 415      _ ≤ Real.exp 0.224 := by linarith
 416  rw [h_log10_eq]
 417  constructor
 418  · -- 2.30 ≤ 3*log(2) + log(5/4)
 419    -- 3 * 0.6931471803 + 0.223 = 2.3024415409 > 2.30
 420    have h1 : (3 : ℝ) * 0.6931471803 + 0.223 > 2.30 := by norm_num
 421    have h2 : 3 * log 2 + log (5/4) > 3 * 0.6931471803 + 0.223 := by linarith
 422    linarith
 423  · -- 3*log(2) + log(5/4) ≤ 2.31
 424    -- 3 * 0.6931471808 + 0.224 = 2.3034415424 < 2.31
 425    have h1 : (3 : ℝ) * 0.6931471808 + 0.224 < 2.31 := by norm_num
 426    have h2 : 3 * log 2 + log (5/4) < 3 * 0.6931471808 + 0.224 := by linarith
 427    linarith
 428
 429end IndisputableMonolith.Numerics