theorem
proved
tactic proof
log_phi_lt_0483
show as:
view Lean formalization →
formal statement (Lean)
279theorem log_phi_lt_0483 : log Real.goldenRatio < (0.483 : ℝ) := by
proof body
Tactic-mode proof.
280 -- Equivalent to: φ < exp(0.483)
281 rw [Real.log_lt_iff_lt_exp Real.goldenRatio_pos]
282 -- Use Taylor bound for exp(0.483): exp(x) ≥ S_10 - error
283 have hx_abs : |(0.483 : ℝ)| ≤ 1 := by norm_num
284 have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
285 have h_abs := abs_sub_le_iff.mp h_bound
286 -- h_abs.2: S_10 - exp ≤ error, i.e., S_10 - error ≤ exp
287 have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.483 : ℝ)^m / m.factorial) =
288 (exp_taylor_10_at_0483 : ℝ) := by
289 simp only [exp_taylor_10_at_0483, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
290 norm_num
291 have h_err_eq : |(0.483 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
292 (exp_error_10_at_0483 : ℝ) := by
293 simp only [abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.483), exp_error_10_at_0483,
294 Nat.factorial, Nat.succ_eq_add_one]
295 norm_num
296 have h_lt := phi_lt_exp_0483
297 have h_lower : (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) ≤
298 Real.exp (0.483 : ℝ) := by
299 have h2 := h_abs.2
300 simp only [h_taylor_eq] at h2
301 linarith
302 calc Real.goldenRatio
303 < (1.6180340 : ℝ) := phi_lt_16180340
304 _ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num
305 _ < (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) := by
306 have h_cast : ((16180340 / 10000000 : ℚ) : ℝ) + (exp_error_10_at_0483 : ℝ) <
307 (exp_taylor_10_at_0483 : ℝ) := by exact_mod_cast h_lt
308 linarith
309 _ ≤ Real.exp (0.483 : ℝ) := h_lower
310
311/-- log(φ) is contained in logPhiInterval - PROVEN using Taylor series bounds -/