alpha_seed_lt

formal source

  23  linarith
  24
  25/-- alpha_seed = 4π·11 < 138.230092 -/
  26theorem alpha_seed_lt : alpha_seed < (138.230092 : ℝ) := by
  27  simp only [alpha_seed]
  28  have h := Real.pi_lt_d6
  29  linarith
  30
  31/-! ## f_gap bounds -/
  32
  33private def exp_taylor_10_at_048 : ℚ :=
  34  let x : ℚ := (48 : ℚ) / 100
  35  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
  36
  37private def exp_error_10_at_048 : ℚ :=
  38  let x : ℚ := (48 : ℚ) / 100
  39  x^10 * 11 / (Nat.factorial 10 * 10)
  40
  41private lemma exp_048_taylor_ceiling :
  42    exp_taylor_10_at_048 + exp_error_10_at_048 < (16161 / 10000 : ℚ) := by
  43  native_decide
  44
  45private lemma exp_048_lt : Real.exp (0.48 : ℝ) < (((16161 / 10000 : ℚ) : ℝ)) := by
  46  have hx_abs : |(0.48 : ℝ)| ≤ 1 := by norm_num
  47  have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
  48  have h_abs := abs_sub_le_iff.mp h_bound
  49  have h_taylor_eq :
  50      (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) =
  51        (exp_taylor_10_at_048 : ℝ) := by
  52    simp only [exp_taylor_10_at_048, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
  53    norm_num
  54  have h_err_eq :
  55      |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
  56        (exp_error_10_at_048 : ℝ) := by