exp_error_10_at_0483

formal source

 264  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
 265
 266/-- Error bound for Taylor at x = 483/1000 -/
 267private def exp_error_10_at_0483 : ℚ :=
 268  let x : ℚ := 483 / 1000
 269  x^10 * 11 / (Nat.factorial 10 * 10)
 270
 271/-- φ < exp(0.483) (via Taylor bound + φ upper bound) -/
 272private lemma phi_lt_exp_0483 : 16180340 / 10000000 + exp_error_10_at_0483 < exp_taylor_10_at_0483 := by
 273  native_decide
 274
 275/-- Rigorous upper bound: log(φ) < 0.483
 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 : ℝ) ≤