Ramanujan.ex_pi_gt_nonneg

theorem ex_pi_gt_nonneg    (m_a x_a : ℝ)    (hm : 0 ≤ m_a)    (hlower : ∀ x > x_a,      x * ∑ k ∈ Finset.range 5, (k.factorial / log x ^ (k + 1))        + (m_a * x / log x ^ 6) < pi x) :    ∀ x > exp 1 * x_a,      exp 1 * x / log x * pi (x / exp 1) >        x ^ 2 * (          1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5          + 65 / log x ^ 6 + ε' m_a x / log x ^ 7) := by  intro x hx  have hxa_ge_one : 1 ≤ x_a := by    by_contra hxa    have hlt : x_a < 1 := lt_of_not_ge hxa    have hbad := hlower 1 hlt    have hpi1 : pi 1 = 0 := by      unfold _root_.pi      norm_num    have hleft0 :        (1 : ℝ) * ∑ k ∈ Finset.range 5, (k.factorial / log (1 : ℝ) ^ (k + 1))          + (m_a * (1 : ℝ) / log (1 : ℝ) ^ 6) = 0 := by      norm_num    linarith  have hxe : exp 1 < x := by    have h1 : exp 1 ≤ exp 1 * x_a := by      nlinarith [hxa_ge_one, exp_pos (1 : ℝ)]    grind  have hlog_gt1 : 1 < log x := by    simpa using log_lt_log (show 0 < exp 1 by positivity) hxe  have hlog_pos : 0 < log x := by linarith  have hx_pos : 0 < x := lt_trans (exp_pos 1) hxe  have hy_gt : x / exp 1 > x_a := by    have hmul : x_a * exp 1 < x := by simpa [mul_comm] using hx    exact (lt_div_iff₀ (exp_pos 1)).2 hmul  have hlow := hlower (x / exp 1) hy_gt  have hmul_pos : 0 < exp 1 * x / log x :=    div_pos (mul_pos (exp_pos 1) hx_pos) hlog_pos  have hmul := mul_lt_mul_of_pos_left hlow hmul_pos  have hlog_div : log (x / exp 1) = log x - 1 := by    rw [log_div (show x ≠ 0 by linarith) (show exp 1 ≠ 0 by positivity), log_exp]  have hfrom0 :      exp 1 * x / log x *        ((x / exp 1) * ∑ k ∈ Finset.range 5, (k.factorial / (log x - 1) ^ (k + 1))          + (m_a * (x / exp 1) / (log x - 1) ^ 6))      < exp 1 * x / log x * pi (x / exp 1) := by    simpa [hlog_div] using hmul  let S : ℝ := ∑ k ∈ Finset.range 5, (k.factorial / (log x - 1) ^ (k + 1))  have hfrom :      x ^ 2 * ((1 / log x) * (S + m_a / (log x - 1) ^ 6))      < exp 1 * x / log x * pi (x / exp 1) := by    have hleft :        exp 1 * x / log x * ((x / exp 1) * S + (m_a * (x / exp 1) / (log x - 1) ^ 6))        = x ^ 2 * ((1 / log x) * (S + m_a / (log x - 1) ^ 6)) := by      field_simp [hlog_pos.ne', show (exp 1 : ℝ) ≠ 0 by positivity]    simpa [S, hleft] using hfrom0  have hsum :      S =        1 / (log x - 1) + 1 / (log x - 1) ^ 2 + 2 / (log x - 1) ^ 3 +        6 / (log x - 1) ^ 4 + 24 / (log x - 1) ^ 5 := by    dsimp [S]    simp [Finset.sum_range_succ, Nat.factorial]  have hfac :      (1 / log x) * S      ≥      1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6        + (206 + 364 / log x + 381 / log x ^ 2 + 238 / log x ^ 3 + 97 / log x ^ 4 +            30 / log x ^ 5 + 8 / log x ^ 6) / log x ^ 7 := by    simpa [hsum] using shift_factorial_lower (log x) hlog_gt1  have hmterm :      m_a / (log x * (log x - 1) ^ 6)      ≥ m_a / log x ^ 7 := by    simpa using shift_m_lower_of_nonneg m_a (log x) hm hlog_gt1  have hcore65 :      (1 / log x) * (S + m_a / (log x - 1) ^ 6)      ≥      1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6        + ε' m_a x / log x ^ 7 := by    have hsplit :        (1 / log x) * (S + m_a / (log x - 1) ^ 6)        = (1 / log x) * S + m_a / (log x * (log x - 1) ^ 6) := by      calc        (1 / log x) * (S + m_a / (log x - 1) ^ 6)            = (1 / log x) * S + (1 / log x) * (m_a / (log x - 1) ^ 6) := by ring        _ = (1 / log x) * S + m_a / (log x * (log x - 1) ^ 6) := by          field_simp [hlog_pos.ne']    have hsum' := add_le_add hfac hmterm    have hsum'' :        1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6          + (206 + 364 / log x + 381 / log x ^ 2 + 238 / log x ^ 3 + 97 / log x ^ 4 +              30 / log x ^ 5 + 8 / log x ^ 6) / log x ^ 7          + m_a / log x ^ 7        ≤ (1 / log x) * (S + m_a / (log x - 1) ^ 6) := by      calc        1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6          + (206 + 364 / log x + 381 / log x ^ 2 + 238 / log x ^ 3 + 97 / log x ^ 4 +              30 / log x ^ 5 + 8 / log x ^ 6) / log x ^ 7          + m_a / log x ^ 7            ≤ (1 / log x) * S + m_a / (log x * (log x - 1) ^ 6) := hsum'        _ = (1 / log x) * (S + m_a / (log x - 1) ^ 6) := hsplit.symm    calc      1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6        + ε' m_a x / log x ^ 7          =            1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6              + (206 + 364 / log x + 381 / log x ^ 2 + 238 / log x ^ 3 + 97 / log x ^ 4 +                  30 / log x ^ 5 + 8 / log x ^ 6) / log x ^ 7              + m_a / log x ^ 7 := by                simp [ε']                ring      _ ≤ (1 / log x) * (S + m_a / (log x - 1) ^ 6) := hsum''  have htarget_le :      x ^ 2 *          (1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6 +            ε' m_a x / log x ^ 7)      ≤ x ^ 2 * ((1 / log x) * (S + m_a / (log x - 1) ^ 6)) :=    mul_le_mul_of_nonneg_left hcore65 (sq_nonneg x)  grind