exp_four_upper

formal source

 282
 283/-! ### Rigorous closures for the φ-endpoint seam bounds -/
 284
 285private lemma exp_four_upper : Real.exp (4 : ℝ) < (54.598151 : ℝ) := by
 286  have hpow : (Real.exp (1 : ℝ)) ^ (4 : ℕ) ≤ (2.7182818286 : ℝ) ^ (4 : ℕ) := by
 287    exact pow_le_pow_left₀ (Real.exp_pos (1 : ℝ)).le (Real.exp_one_lt_d9).le 4
 288  have hnum : (2.7182818286 : ℝ) ^ (4 : ℕ) < (54.598151 : ℝ) := by norm_num
 289  have hEq : Real.exp (4 : ℝ) = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by
 290    calc
 291      Real.exp (4 : ℝ) = Real.exp ((4 : ℕ) * (1 : ℝ)) := by norm_num
 292      _ = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by simpa using (Real.exp_nat_mul (1 : ℝ) 4)
 293  rw [hEq]
 294  exact lt_of_le_of_lt hpow hnum
 295
 296private lemma exp_four_lower : (54.598150 : ℝ) < Real.exp (4 : ℝ) := by
 297  have hpow : (2.7182818283 : ℝ) ^ (4 : ℕ) < (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by
 298    exact pow_lt_pow_left₀ Real.exp_one_gt_d9 (by norm_num) (by norm_num : (4 : ℕ) ≠ 0)
 299  have hnum : (54.598150 : ℝ) < (2.7182818283 : ℝ) ^ (4 : ℕ) := by norm_num
 300  have hEq : Real.exp (4 : ℝ) = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by
 301    calc
 302      Real.exp (4 : ℝ) = Real.exp ((4 : ℕ) * (1 : ℝ)) := by norm_num
 303      _ = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by simpa using (Real.exp_nat_mul (1 : ℝ) 4)
 304  have hpow' : (2.7182818283 : ℝ) ^ (4 : ℕ) < Real.exp (4 : ℝ) := by
 305    rw [hEq]
 306    exact hpow
 307  exact lt_trans hnum hpow'
 308
 309private def exp_taylor_10_at_081416924 : ℚ :=
 310  let x : ℚ := 81416924 / 100000000
 311  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
 312
 313private def exp_error_10_at_081416924 : ℚ :=
 314  let x : ℚ := 81416924 / 100000000
 315  x^10 * 11 / (Nat.factorial 10 * 10)