 355    exact le_of_lt h1
 356
 357/-- Interval containing log(10) ≈ 2.3025 -/
 358def log10Interval : Interval where
 359  lo := 230 / 100
 360  hi := 231 / 100
 361  valid := by norm_num
 362
 363/-- log(10) is contained in log10Interval.
 364    Proof using log(10) = log(2) + log(5) and Mathlib bounds.
 365    log(2) ≈ 0.693, log(5) = log(10/2) requires log(10).
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.