RS_prime.meisselMertensConstant_identity

theorem meisselMertensConstant_identity {x : ℝ} (hx : 2 ≤ x) :    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) =    log (log x) + meisselMertensConstant + (θ x - x) / (x * log x) +    ∫ y in Set.Ioi x, (θ y - y) * deriv (fun s ↦ 1 / s / Real.log s) y := by  have integral_eq_loglog : ∫ y in 2..x, 1 / y / log y = log (log x) - log (log 2) := by    have {y} (hy : y ∈ Set.uIcc 2 x) := (Set.uIcc_of_le hx ▸ hy).1    have {y} (hy : y ∈ Set.uIcc 2 x) : log y ≠ 0 :=      log_ne_zero_of_pos_of_ne_one (by grind) (by grind)    refine intervalIntegral.integral_eq_sub_of_hasDerivAt (f := Real.log ∘ log) (fun y hy => ?_) ?_    · convert! (hasDerivAt_log (this hy)).comp y (hasDerivAt_log (by grind)) using 1      field_simp    · exact ContinuousOn.intervalIntegrable_of_Icc hx (by fun_prop (disch := aesop))  rw [eq_415 (by fun_prop (disch := grind)) hx integrableOn_deriv_inv_div_log.1    (integrableOn_deriv_inv_div_log.2 x hx), integral_eq_loglog, meisselMertensConstant]  ring