Ramanujan.Calculations.B_le_small_of

theorem B_le_small_of    {xₐ : ℝ}    (hxₐ : xₐ = exp (3914 : ℝ))    (hlogxₐ : log xₐ = (3914 : ℝ)) :    1 / log xₐ + 7 * 2 ^ 8 / log xₐ ^ 2      + 7 * log xₐ ^ 6 / (sqrt xₐ * (log 2) ^ 8)      ≤ (3 : ℝ) / 8000 := by  rw [hlogxₐ]  rw [hxₐ, sqrt_exp_3914]  have htail : 7 * (3914 : ℝ) ^ 6 / (exp (1957 : ℝ) * (log 2) ^ 8) ≤ (1 : ℝ) / 1000000 := by    rw [show 7 * (3914 : ℝ) ^ 6 / (exp (1957 : ℝ) * (log 2) ^ 8) =      7 * (3914 : ℝ) ^ 6 * exp (-(1957 : ℝ)) / (log 2) ^ 8 by      field_simp [(show (0 : ℝ) < exp (1957 : ℝ) by positivity).ne']      rw [show (1 : ℝ) = exp (1957 : ℝ) * exp (-(1957 : ℝ)) by rw [← exp_add]; norm_num]]    exact tail_small  linarith [htail, show (1 / (3914 : ℝ) + 7 * 2 ^ 8 / (3914 : ℝ) ^ 2 +    (1 : ℝ) / 1000000) ≤ (3 : ℝ) / 8000 by norm_num]