RS_prime.eq_414

@[blueprint  "rs-414"  (title := "RS equation (4.14)")  (statement := /--  $$\sum_{p \leq x} f(p) = \int_2^x \frac{f(y)\ dy}{\log y} + \frac{2 f(2)}{\log 2} $$  $$ + \frac{f(x) (\vartheta(x) - x)}{\log x} - \int_2^x (\vartheta(y) - y) \frac{d}{dy}( \frac{f(y)}{\log y} )\ dy.$$ -/)  (proof := /-- Follows from Sublemma \ref{rs-413} and integration by parts. -/)  (latexEnv := "sublemma")  (discussion := 600)]theorem eq_414 {f : ℝ → ℝ} {x : ℝ} (hx : 2 ≤ x) (hf : ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ f t)    (hd : IntervalIntegrable (fun t => deriv (fun s ↦ f s / log s) t) volume 2 x) :    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), f p =    (∫ y in 2..x, f y / log y) + 2 * f 2 / Real.log 2 +    f x * (θ x - x) / log x -    ∫ y in 2..x, (θ y - y) * deriv (fun s ↦ f s / log s) y :=  let hcc := Set.uIcc_of_le hx  let hoc := Set.uIoc_of_le hx  have hm : Set.Ioo 2 x ∈ ae (volume.restrict (Set.Ioc 2 x)) := by    by_cases hp : 2 < x    · rw [mem_ae_iff, Measure.restrict_apply' measurableSet_Ioc, ← Set.sdiff_eq_compl_inter,        Ioc_diff_Ioo_right hp, volume_singleton]    · simp_all  have hae : (fun t ↦ deriv (fun s ↦ f s / log s) t) =ᶠ[ae (volume.restrict (Set.Ioc 2 x))]    derivWithin (fun t ↦ f t / log t) (Set.uIcc 2 x) := by    filter_upwards [hm] with y hy    have : Set.Icc 2 x ∈ 𝓝 y := mem_nhds_iff.2      ⟨Set.Ioo 2 x, Set.Ioo_subset_Icc_self, ⟨isOpen_Ioo, hy⟩⟩    refine (DifferentiableAt.derivWithin ?_ (uniqueDiffWithinAt_of_mem_nhds (hcc ▸ this))).symm    refine (hf y (Set.Ioo_subset_Icc_self hy)).fun_div      (differentiableAt_log (by simp_all; linarith)) ?_    linarith [Real.log_pos (by simp_all; linarith)]  calc  _ = f x * (θ x - x) / log x + x * f x / log x -    (∫ y in 2..x, (θ y - y) * deriv (fun t ↦ f t / log t) y) -    ∫ y in 2..x, y * deriv (fun t ↦ f t / log t) y := by    rw [eq_413 hx hf hd, ← tsub_add_eq_tsub_tsub, ← intervalIntegral.integral_add _      (hd.continuousOn_mul (by fun_prop))]    · ring_nf    · refine (intervalIntegrable_iff_integrableOn_Ioc_of_le hx).2 ?_      have hb : ∀ᵐ y ∂volume.restrict (Set.Ioc 2 x), ‖θ y - y‖ ≤ θ x + x := by        refine ae_restrict_of_forall_mem measurableSet_Ioc (fun y hy => ?_)        calc        _ ≤ ‖θ y‖ + ‖y‖ := by bound        _ = θ y + y := by rw [norm_of_nonneg (theta_nonneg y), norm_of_nonneg (by grind : 0 ≤ y)]        _ ≤ θ x + x := add_le_add (theta_mono hy.2) hy.2      exact ((intervalIntegrable_iff_integrableOn_Ioc_of_le hx).1 hd).bdd_mul        (theta_mono.measurable.aestronglyMeasurable.sub (by fun_prop)) hb  _ = f x * (θ x - x) / log x +    ((∫ y in 2..x, 1 * (f y / log y) + y * derivWithin (fun t ↦ f t / log t) (Set.uIcc 2 x) y) +    2 * f 2 / log (2 : ℝ)) -    (∫ y in 2..x, (θ y - y) * deriv (fun t ↦ f t / log t) y) -    ∫ y in 2..x, y * deriv (fun t ↦ f t / log t) y := by    rw [← sub_add_cancel (x * f x / log x) (2 * f 2 / log (2 : ℝ)),      intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivWithinAt, mul_div, mul_div]    · intro y _; exact (hasDerivAt_id' y).hasDerivWithinAt    · refine fun y hy ↦ (hf y (hcc ▸ hy)|>.fun_div ?_ ?_).differentiableWithinAt.hasDerivWithinAt      · exact differentiableAt_log (by simp_all; linarith)      · linarith [Real.log_pos (by simp_all; linarith)]    · exact intervalIntegrable_const    · exact hd.congr_ae (hoc ▸ hae)  _ = f x * (θ x - x) / log x +    ((∫ y in 2..x, f y / log y) + (∫ y in 2..x, y * deriv (fun t ↦ f t / log t) y) +    2 * f 2 / log (2 : ℝ)) -    (∫ y in 2..x, (θ y - y) * deriv (fun t ↦ f t / log t) y) -    ∫ y in 2..x, y * deriv (fun t ↦ f t / log t) y := by    have : (fun y ↦ y * deriv (fun t ↦ f t / log t) y) =ᶠ[ae (volume.restrict (Set.Ioc 2 x))]      fun y ↦ y * derivWithin (fun t ↦ f t / log t) (Set.uIcc 2 x) y := by      filter_upwards [Filter.eventually_iff.1 hae.eventually] with y hy      grind    have hi := intervalIntegral.integral_congr_ae_restrict (hoc ▸ this)    simp only [one_mul, sub_left_inj, add_right_inj, add_left_inj, hi]    refine intervalIntegral.integral_add (ContinuousOn.intervalIntegrable_of_Icc hx ?_) ?_    · refine ContinuousOn.div₀ ?_ (continuousOn_log.mono (by grind))        (fun x hx => by linarith [Real.log_pos (by simp_all; linarith)])      exact fun y hy ↦ (hf y hy).continuousAt.continuousWithinAt    · exact (hd.continuousOn_mul (by fun_prop)).congr_ae (hoc ▸ this)  _ = _ := by ring