exp_error_10_at_0481

formal source

 224  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
 225
 226/-- Error bound for Taylor at x = 481/1000. -/
 227private def exp_error_10_at_0481 : ℚ :=
 228  let x : ℚ := 481 / 1000
 229  x^10 * 11 / (Nat.factorial 10 * 10)
 230
 231/-- exp(0.481) < φ (via Taylor bound + φ lower bound). -/
 232private lemma exp_0481_lt_phi : exp_taylor_10_at_0481 + exp_error_10_at_0481 < 161803395 / 100000000 := by
 233  native_decide
 234
 235/-- Rigorous lower bound: log(φ) > 0.481.
 236
 237    Proof using exp monotonicity: log(φ) > 0.481 ↔ φ > exp(0.481).
 238    We have φ > 1.61803395 and exp(0.481) ≈ 1.617691... < 1.61803395. -/
 239theorem log_phi_gt_0481 : (0.481 : ℝ) < log Real.goldenRatio := by
 240  rw [Real.lt_log_iff_exp_lt Real.goldenRatio_pos]
 241  have hx_pos : (0 : ℝ) ≤ (0.481 : ℝ) := by norm_num
 242  have hx_le1 : (0.481 : ℝ) ≤ 1 := by norm_num
 243  have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
 244  have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.481 : ℝ)^m / m.factorial) =
 245      (exp_taylor_10_at_0481 : ℝ) := by
 246    simp only [exp_taylor_10_at_0481, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 247    norm_num
 248  have h_err_eq : (0.481 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) =
 249      (exp_error_10_at_0481 : ℝ) := by
 250    simp only [exp_error_10_at_0481, Nat.factorial]
 251    norm_num
 252  have h_lt := exp_0481_lt_phi
 253  calc Real.exp (0.481 : ℝ)
 254      ≤ (∑ m ∈ Finset.range 10, (0.481 : ℝ)^m / m.factorial) +
 255        (0.481 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) := h_bound
 256    _ = (exp_taylor_10_at_0481 : ℝ) + (exp_error_10_at_0481 : ℝ) := by rw [h_taylor_eq, h_err_eq]
 257    _ < ((161803395 / 100000000 : ℚ) : ℝ) := by exact_mod_cast h_lt