Ramanujan.pi_lower

@[blueprint  "ramanujan-pi-lower"  (title := "Lower bound for pi")  (statement := /-- Suppose that for $x \geq 2$ we have $|\theta(x)-x|\log^{5} x\leq x a(x)$. Then$$\pi(x)\geq \frac{x}{\log x} -a(x)\frac{x}{\log^6 x}+\int_2^x\frac{d t}{\log^2 t}-\int_2^x\frac{a(t)}{\log^7 t}\ dt.$$ (cf. \cite[\S 5]{PT2021})-/)  (proof := /-- Follows from Lemma \ref{pi-error-identity} and the triangle inequality. -/)  (latexEnv := "sublemma")  (discussion := 989)]theorem pi_lower (a : ℝ → ℝ) (htheta : ∀ x ≥ 2, |θ x - x| * log x ^ 5 ≤ x * a x) (x : ℝ)    (ha : IntegrableOn (fun t ↦ a t / log t ^ 7) (Icc 2 x) volume)    (hx : 2 ≤ x) :    pi x ≥ x / log x - a x * x / log x ^ 6 + (∫ t in Icc 2 x, 1 / log t ^ 2) - ∫ t in Icc 2 x, a t / log t ^ 7 := by  have h1 : (θ x - x) / log x ≥ - (x * a x / log x ^ 6) := by    have hlog_pos : 0 < log x := log_pos (by linarith)    have h1a : (θ x - x) / log x ≥ - (|θ x - x| / log x) := by      have h1a1 : - |θ x - x| ≤ (θ x - x) := neg_abs_le (θ x - x)      have h : (- |θ x - x|) / log x ≤ (θ x - x) / log x := div_le_div_of_nonneg_right h1a1 hlog_pos.le      have h' : (- |θ x - x|) / log x = - (|θ x - x| / log x) := by field_simp [hlog_pos.ne']      rw [h'] at h; exact h.ge    have h1b : |θ x - x| * log x ^ 5 ≤ x * a x := htheta x hx    have h1c : |θ x - x| / log x ≤ (x * a x) / log x ^ 6 := by      have h1c1 : |θ x - x| ≤ (x * a x) / log x ^ 5 := by        have h1c2 : 0 < log x ^ 5 := by positivity        calc          |θ x - x| = (|θ x - x| * log x ^ 5) / log x ^ 5 := by field_simp [hlog_pos.ne']          _ ≤ (x * a x) / log x ^ 5 := by gcongr      calc        |θ x - x| / log x ≤ ((x * a x) / log x ^ 5) / log x := by gcongr        _ = (x * a x) / log x ^ 6 := by field_simp [pow_succ, hlog_pos.ne']    have h1d : - (|θ x - x| / log x) ≥ - ((x * a x) / log x ^ 6) := by gcongr    linarith  have h_int_abs : IntegrableOn (fun t : ℝ ↦ |(θ t - t) / (t * log t ^ 2)|) (Icc 2 x) volume := integrable_theta x |>.abs  have h_neg_abs_int : IntegrableOn (fun t : ℝ ↦ - |(θ t - t) / (t * log t ^ 2)|) (Icc 2 x) volume := h_int_abs.neg  have h2a : ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) ≥ - (∫ t in Icc 2 x, |(θ t - t) / (t * log t ^ 2)|) := by    have h2a1 : ∀ t ∈ Icc 2 x, - |(θ t - t) / (t * log t ^ 2)| ≤ (θ t - t) / (t * log t ^ 2) := fun t _ => neg_abs_le _    have h2a2 : ∫ t in Icc 2 x, (- |(θ t - t) / (t * log t ^ 2)|) ≤ ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) :=      MeasureTheory.setIntegral_mono_on h_neg_abs_int (integrable_theta x) measurableSet_Icc h2a1    have h2a3 : ∫ t in Icc 2 x, (- |(θ t - t) / (t * log t ^ 2)|) = - (∫ t in Icc 2 x, |(θ t - t) / (t * log t ^ 2)|) := by rw [MeasureTheory.integral_neg]    rw [h2a3] at h2a2; exact h2a2.ge  have h2b : ∫ t in Icc 2 x, |(θ t - t) / (t * log t ^ 2)| ≤ ∫ t in Icc 2 x, a t / log t ^ 7 :=    MeasureTheory.setIntegral_mono_on h_int_abs ha measurableSet_Icc (fun t ht => by      have ht2 : 2 ≤ t := ht.1      have hlog_t_pos : 0 < log t := log_pos (by linarith)      have h71 : |θ t - t| * log t ^ 5 ≤ t * a t := htheta t ht2      have h72 : |θ t - t| ≤ (t * a t) / log t ^ 5 := by        have h : 0 < log t ^ 5 := by positivity        calc          |θ t - t| = (|θ t - t| * log t ^ 5) / log t ^ 5 := by field_simp [hlog_t_pos.ne']          _ ≤ (t * a t) / log t ^ 5 := by gcongr      have h73 : |(θ t - t) / (t * log t ^ 2)| = |θ t - t| / (t * log t ^ 2) := by        have h_t_pos : 0 < t := by linarith        rw [abs_div, abs_of_pos (show 0 < t * log t ^ 2 from by positivity)]      rw [h73]      calc        |θ t - t| / (t * log t ^ 2) ≤ ((t * a t) / log t ^ 5) / (t * log t ^ 2) := by gcongr        _ = (t * a t) / (t * log t ^ 7) := by field_simp [pow_succ, hlog_t_pos.ne']        _ = a t / log t ^ 7 := by          have h_t_pos : 0 < t := by linarith          field_simp [h_t_pos.ne'])  have h2c : - (∫ t in Icc 2 x, |(θ t - t) / (t * log t ^ 2)|) ≥ - (∫ t in Icc 2 x, a t / log t ^ 7) := by gcongr  have h2 : ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) ≥ - (∫ t in Icc 2 x, a t / log t ^ 7) := by linarith  calc    pi x = x / log x + (θ x - x) / log x + (∫ t in Icc 2 x, 1 / log t ^ 2) + ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) := by      have h_eq1 : pi x - Li x = (θ x - x) / log x + 2 / log 2 + ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) := pi_error_identity x hx      have h_eq2 : Li x = x / log x - 2 / log 2 + ∫ t in Icc 2 x, 1 / log t ^ 2 := Li_eq_sub_add_integral x hx      linarith    _ ≥ x / log x + (- (x * a x / log x ^ 6)) + (∫ t in Icc 2 x, 1 / log t ^ 2) + (- (∫ t in Icc 2 x, a t / log t ^ 7)) := by      gcongr    _ = x / log x - a x * x / log x ^ 6 + (∫ t in Icc 2 x, 1 / log t ^ 2) - ∫ t in Icc 2 x, a t / log t ^ 7 := by ring