Ramanujan.pi_bound

@[blueprint  "pt_eq_18"  (title := "Equation (18) of Platt-Trudgian")  (statement := /-- For $x \geq 2$ we have$$E_\theta(x) (\log x)^5 \leq a(x).$$-/)  (proof := /-- This follows from the previous five sublemmas. -/)  (latexEnv := "proposition")  (discussion := 994)]theorem pi_bound (x : ℝ) (hx : 2 ≤ x) :    Eθ x * ( log x)^5 ≤ a x := by  set b : ℝ :=    if x ∈ Set.Ico 2 599 then 1 - log 2 / 3    else if x ∈ Set.Ico 599 (exp 58) then log x ^ 2 / (8 * π * sqrt x)    else if x ∈ Set.Ico (exp 58) (exp 1169) then sqrt (8 / (17 * π)) * (log x / 6.455) ^ (1 / 4 : ℝ) * exp (-sqrt (log x / 6.455))    else if x ∈ Set.Ico (exp 1169) (exp 2000) then 462.0 * (log x / 5.573412) ^ (1.52 : ℝ) * exp (-1.89 * sqrt (log x / 5.573412))    else if x ∈ Set.Ico (exp 2000) (exp 3000) then 411.5 * (log x / 5.573412) ^ (1.52 : ℝ) * exp (-1.89 * sqrt (log x / 5.573412))    else 379.7 * (log x / 5.573412) ^ (1.52 : ℝ) * exp (-1.89 * sqrt (log x / 5.573412))  have ha : a x = (log x) ^ 5 * b := by    simp [a, b]  have hb : Eθ x ≤ b := by    by_cases h1 : x ∈ Set.Ico 2 599    · simpa [b, h1] using pi_bound_1 x h1    · have hx599 : (599 : ℝ) ≤ x := by        by_contra hx599        exact h1 ⟨hx, lt_of_not_ge hx599⟩      by_cases h2 : x ∈ Set.Ico 599 (exp 58)      · simpa [b, h1, h2] using pi_bound_2 x h2      · have hx58 : exp 58 ≤ x := by          by_contra hx58          exact h2 ⟨hx599, lt_of_not_ge hx58⟩        by_cases h3 : x ∈ Set.Ico (exp 58) (exp 1169)        · simpa [b, h1, h2, h3] using pi_bound_3 x h3        · have hx1169 : exp 1169 ≤ x := by            by_contra hx1169            exact h3 ⟨hx58, lt_of_not_ge hx1169⟩          by_cases h4 : x ∈ Set.Ico (exp 1169) (exp 2000)          · simpa [b, h1, h2, h3, h4] using pi_bound_4 x h4          · have hx2000 : exp 2000 ≤ x := by              by_contra hx2000              exact h4 ⟨hx1169, lt_of_not_ge hx2000⟩            by_cases h5 : x ∈ Set.Ico (exp 2000) (exp 3000)            · simpa [b, h1, h2, h3, h4, h5] using pi_bound_5 x h5            · have hx3000 : exp 3000 ≤ x := by                by_contra hx3000                exact h5 ⟨hx2000, lt_of_not_ge hx3000⟩              simpa [b, h1, h2, h3, h4, h5] using pi_bound_6 x hx3000  simpa [ha, mul_assoc, mul_left_comm, mul_comm] using    mul_le_mul_of_nonneg_right hb (pow_nonneg (log_nonneg (by linarith : 1 ≤ x)) 5)