log_phi_lt_0483

formal source

 276
 277    Proof using exp monotonicity: log(φ) < 0.483 ↔ φ < exp(0.483).
 278    We have φ < 1.6180340 and exp(0.483) ≈ 1.6210... > 1.6180340. -/
 279theorem log_phi_lt_0483 : log Real.goldenRatio < (0.483 : ℝ) := by
 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