theorem
proved
log_10_in_interval
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Numerics.Interval.Log on GitHub at line 369.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
366 Instead: log(10) = 2*log(√10), but √10 computation is circular.
367 Best approach: log(10) = log(2) + log(5) where log(5) = log(4*5/4) = 2*log(2) + log(1.25)
368 So log(10) = 3*log(2) + log(1.25) -/
369theorem log_10_in_interval : log10Interval.contains (log 10) := by
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