Ramanujan.pi_bound_2

@[blueprint  "ramanujan-pibound-2"  (title := "Error estimate for theta, range 2 ")  (statement := /-- For $599 < x \leq \exp(58)$ we have$$E_\theta(x) \leq \frac{\log^2 x}{8\pi\sqrt{x}}.$$(cf. \cite[(18)]{PT2021})-/)  (proof := /-- This is \cite[Lemma 6]{PT2021}. -/)  (latexEnv := "sublemma")]theorem pi_bound_2 (x : ℝ) (hx : x ∈ Set.Ico 599 (exp 58)) :    Eθ x ≤ log x ^ 2 / (8 * π * sqrt x) := by  obtain ⟨hx_lo, hx_hi⟩ := hx  have hx_pos : (0 : ℝ) < x := by linarith  by_cases! hx_gt : x > 599  · have hlog_pos : (0 : ℝ) < log x := log_pos (by linarith : (1 : ℝ) < x)    have hlog_x_ge : 6 < log x := by      have hexp6_lt : exp (6 : ℝ) < x := by        have : exp (6 : ℝ) = exp (1 : ℝ) ^ (6 : ℕ) := by rw [← exp_nat_mul]; ring_nf        rw [this]        calc (exp 1 : ℝ) ^ 6 < (2.7182818286 : ℝ) ^ 6 := by gcongr; exact exp_one_lt_d9          _ < 599 := by norm_num          _ < x := hx_gt      exact (Real.lt_log_iff_exp_lt hx_pos).mpr hexp6_lt    have hrh : 4.92 * sqrt (x / log x) < 3e12 := by      suffices h : 4.92 ^ 2 * x < (3e12) ^ 2 * log x by        have h1 : 4.92 ^ 2 * (x / log x) < (3e12) ^ 2 := by          rw [show 4.92 ^ 2 * (x / log x) = 4.92 ^ 2 * x / log x from by ring]          rw [div_lt_iff₀ hlog_pos]          exact h        have h2 := sqrt_lt_sqrt (by positivity : 0 ≤ 4.92 ^ 2 * (x / log x)) h1        rw [sqrt_sq (by positivity : (0 : ℝ) ≤ 3e12)] at h2        calc 4.92 * sqrt (x / log x) = sqrt (4.92 ^ 2 * (x / log x)) := by              rw [sqrt_mul (by positivity : (0 : ℝ) ≤ 4.92 ^ 2), sqrt_sq (by positivity : (0 : ℝ) ≤ 4.92)]          _ < 3e12 := h2      by_cases! hx45 : x ≤ exp 45      · have hexp45 : exp (45 : ℝ) < 2 * 10^20 := by          have : exp (45 : ℝ) = exp (1 : ℝ) ^ (45 : ℕ) := by rw [← exp_nat_mul]; ring_nf          rw [this]          calc (exp 1 : ℝ) ^ 45 < (2.7182818286 : ℝ) ^ 45 := by gcongr; exact exp_one_lt_d9            _ < 2 * 10^20 := by norm_num        have : 4.92 ^ 2 * x ≤ 4.92 ^ 2 * exp 45 := by gcongr        have : 4.92 ^ 2 * exp 45 < 4.92 ^ 2 * (2 * 10^20) := by gcongr        have : 4.92 ^ 2 * (2 * (10 : ℝ) ^ 20) ≤ (3e12) ^ 2 * 6 := by norm_num        have : (3e12) ^ 2 * 6 < (3e12 : ℝ) ^ 2 * log x := by gcongr        linarith      · have hlog45 : 45 < log x := by          rwa [show (45 : ℝ) = log (exp 45) from by rw [log_exp],               log_lt_log_iff (exp_pos 45) hx_pos]        have hexp58 : exp (58 : ℝ) < 16 * 10^24 := by          have h29 : exp (29 : ℝ) < 4 * 10^12 := by            have : exp (29 : ℝ) = exp (1 : ℝ) ^ (29 : ℕ) := by rw [← exp_nat_mul]; ring_nf            rw [this]            calc (exp 1 : ℝ) ^ 29 < (2.7182818286 : ℝ) ^ 29 := by gcongr; exact exp_one_lt_d9              _ < 4 * 10^12 := by norm_num          have : exp (58 : ℝ) = exp (29 : ℝ) * exp (29 : ℝ) := by rw [← exp_add]; norm_num          rw [this]          nlinarith [exp_pos (29 : ℝ)]        have : 4.92 ^ 2 * x < 4.92 ^ 2 * exp 58 := by gcongr        have : 4.92 ^ 2 * exp 58 < 4.92 ^ 2 * (16 * 10^24) := by gcongr        have : 4.92 ^ 2 * (16 * (10 : ℝ) ^ 24) ≤ (3e12) ^ 2 * 45 := by norm_num        have : (3e12) ^ 2 * 45 < (3e12 : ℝ) ^ 2 * log x := by gcongr        linarith    have hbuthe : |θ x - x| ≤ (sqrt x) * (log x) ^ 2 / (8 * π) := by      have hx_nonneg : 0 ≤ x := by linarith      have hx_ne : x ≠ 0 := by linarith      have hlog_ne : log x ≠ 0 := ne_of_gt hlog_pos      have hden_ne : 8 * π ≠ (0 : ℝ) := by positivity      have harg_near : ∀ᶠ y in 𝓝[>] x, 4.92 * sqrt (y / log y) < 3e12 := by        have hcont : ContinuousAt (fun y : ℝ => 4.92 * sqrt (y / log y)) x := by          fun_prop (disch := assumption)        exact (hcont.tendsto.mono_left nhdsWithin_le_nhds).eventually (Iio_mem_nhds hrh)      have hleft : Tendsto (fun y : ℝ => |θ x - y|) (𝓝[>] x) (𝓝 |θ x - x|) := by        have hcont : ContinuousAt (fun y : ℝ => |θ x - y|) x := by fun_prop        exact hcont.tendsto.mono_left nhdsWithin_le_nhds      have hright : Tendsto (fun y : ℝ => (sqrt y) * (log y) ^ 2 / (8 * π)) (𝓝[>] x)          (𝓝 ((sqrt x) * (log x) ^ 2 / (8 * π))) := by        have hcont : ContinuousAt (fun y : ℝ => (sqrt y) * (log y) ^ 2 / (8 * π)) x := by          fun_prop (disch := assumption)        exact hcont.tendsto.mono_left nhdsWithin_le_nhds      refine le_of_tendsto_of_tendsto hleft hright ?_      filter_upwards [Buthe2.eventually_Buthe_theta_eq_theta x hx_nonneg, harg_near,        self_mem_nhdsWithin] with y hy_eq hyT hygt      rw [← hy_eq]      exact Buthe2.theorem_2b y (3e12) PT_theorem_1 hyT.le (by        have hygt' : x < y := hygt        linarith)    unfold Eθ    have hsqrt_pos : (0 : ℝ) < sqrt x := sqrt_pos.mpr hx_pos    have hsqx : sqrt x * sqrt x = x := Real.mul_self_sqrt hx_pos.le    rw [div_le_div_iff₀ hx_pos (by positivity : (0 : ℝ) < 8 * π * sqrt x)]    have h1 :        |θ x - x| * (8 * π * sqrt x) ≤          sqrt x * (log x) ^ 2 / (8 * π) * (8 * π * sqrt x) :=      mul_le_mul_of_nonneg_right hbuthe (by positivity)    have h2 : sqrt x * (log x) ^ 2 / (8 * π) * (8 * π * sqrt x) = log x ^ 2 * x := by      field_simp      nlinarith    linarith  · have hx_eq : x = 599 := le_antisymm hx_gt hx_lo    subst hx_eq    unfold Eθ    have habs :=      LeanCert.CertifiedBounds.Chebyshev.abs_theta_sub_le_mul_of_checkThetaRelErrorReal        599 20 (65 / 1000) (by norm_num) (by norm_num) thetaCheck599 (599 : ℝ) (by norm_num)        (by push_cast; norm_num)    have hEθ : |θ (599 : ℝ) - 599| / 599 ≤ 65 / 1000 := by      rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 599)]      push_cast at habs      exact habs    suffices h_bound : (65 : ℝ) / 1000 ≤ log (599 : ℝ) ^ 2 / (8 * π * sqrt 599) by      linarith    rw [le_div_iff₀ (by positivity : (0 : ℝ) < 8 * π * sqrt 599)]    have hpi : π < 3.1416 := pi_lt_d4    have hsqrt : sqrt (599 : ℝ) < 24.5 := by      rw [show (24.5 : ℝ) = sqrt (24.5 ^ 2) from by rw [sqrt_sq (by norm_num : (0 : ℝ) ≤ 24.5)]]      exact sqrt_lt_sqrt (by norm_num) (by norm_num)    have hlog : (6.39 : ℝ) < log 599 := by      rw [show (6.39 : ℝ) = log (exp 6.39) from by rw [log_exp]]      exact log_lt_log (exp_pos 6.39) (by        have h1 : exp (6.39 : ℝ) = exp 6 * exp (39 / 100 : ℝ) := by rw [← exp_add]; norm_num        rw [h1]        have h2 : exp (6 : ℝ) < 403.5 := by          have : exp (6 : ℝ) = exp (1 : ℝ) ^ (6 : ℕ) := by rw [← exp_nat_mul]; ring_nf          rw [this]          calc (exp 1 : ℝ) ^ 6 < (2.7182818286 : ℝ) ^ 6 := by gcongr; exact exp_one_lt_d9            _ < 403.5 := by norm_num        have h3 : exp (39 / 100 : ℝ) < 1.48 := by          have hx : |((39 : ℝ) / 100)| ≤ 1 := by norm_num          have hbound := exp_bound hx (n := 5) (by norm_num)          simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial] at hbound          push_cast at hbound          rw [abs_le] at hbound          linarith [hbound.2]        nlinarith [exp_pos (6 : ℝ), exp_pos (39 / 100 : ℝ)])    nlinarith [Real.pi_pos, sqrt_nonneg (599 : ℝ), sq_nonneg (log (599 : ℝ) - 6.39)]