SmoothedChebyshevDirichlet

@[blueprint  (title := "SmoothedChebyshevDirichlet")  (statement := /--  We have that  $$\psi_{\epsilon}(X) = \sum_{n=1}^\infty \Lambda(n)\widetilde{1_{\epsilon}}(n/X).$$  -/)  (proof := /--  We have that  $$\psi_{\epsilon}(X) = \frac{1}{2\pi i}\int_{(2)}\sum_{n=1}^\infty \frac{\Lambda(n)}{n^s}  \mathcal{M}(\widetilde{1_{\epsilon}})(s)  X^{s}ds.$$  We have enough decay (thanks to quadratic decay of $\mathcal{M}(\widetilde{1_{\epsilon}})$) to  justify the interchange of summation and integration. We then get  $$\psi_{\epsilon}(X) =  \sum_{n=1}^\infty \Lambda(n)\frac{1}{2\pi i}\int_{(2)}  \mathcal{M}(\widetilde{1_{\epsilon}})(s)  (n/X)^{-s}  ds  $$  and apply the Mellin inversion formula.  -/)]theorem SmoothedChebyshevDirichlet {SmoothingF : ℝ → ℝ}    (diffSmoothingF : ContDiff ℝ 1 SmoothingF)    (SmoothingFpos : ∀ x > 0, 0 ≤ SmoothingF x)    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (mass_one : ∫ x in Ioi (0 : ℝ), SmoothingF x / x = 1)    {X : ℝ} (X_gt : 3 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) :    SmoothedChebyshev SmoothingF ε X =      ∑' n, ArithmeticFunction.vonMangoldt n * Smooth1 SmoothingF ε (n / X) := by  dsimp [SmoothedChebyshev, SmoothedChebyshevIntegrand, VerticalIntegral', VerticalIntegral]  set σ : ℝ := 1 + (Real.log X)⁻¹  have log_gt : 1 < Real.log X := logt_gt_one X_gt.le  have σ_gt : 1 < σ := by    simp only [σ]    have : 0 < (Real.log X)⁻¹ := by      simp only [inv_pos]      linarith    linarith  have σ_le : σ ≤ 2 := by    simp only [σ]    have : (Real.log X)⁻¹ < 1 := inv_lt_one_of_one_lt₀ log_gt    linarith  calc    _ = 1 / (2 * π * I) * (I * ∫ (t : ℝ), ∑' n, Λ n / (n : ℂ) ^ (σ + ↑t * I) *      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) * X ^ (σ + ↑t * I)) := ?_    _ = 1 / (2 * π * I) * (I * ∑' n, ∫ (t : ℝ), Λ n / (n : ℂ) ^ (σ + ↑t * I) *      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) * X ^ (σ + ↑t * I)) := ?_    _ = 1 / (2 * π * I) * (I * ∑' n, Λ n * ∫ (t : ℝ),      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) *        (X / (n : ℂ)) ^ (σ + ↑t * I)) := ?_    _ = 1 / (2 * π) * (∑' n, Λ n * ∫ (t : ℝ),      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) *        (X / (n : ℂ)) ^ (σ + ↑t * I)) := ?_    _ = ∑' n, Λ n * (1 / (2 * π) * ∫ (t : ℝ),      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) *        (X / (n : ℂ)) ^ (σ + ↑t * I)) := ?_    _ = ∑' n, Λ n * (1 / (2 * π) * ∫ (t : ℝ),      mellin (fun x ↦ ↑(Smooth1 SmoothingF ε x)) (σ + ↑t * I) *        ((n : ℂ) / X) ^ (-(σ + ↑t * I))) := ?_    _ = _ := ?_  · congr; ext t    rw [LogDerivativeDirichlet]    · rw [← tsum_mul_right, ← tsum_mul_right]    · simp [σ_gt]  · congr    exact SmoothedChebyshevDirichlet_aux_tsum_integral diffSmoothingF SmoothingFpos      suppSmoothingF mass_one (by linarith) εpos ε_lt_one σ_gt σ_le  · field_simp; congr; ext n; rw [← MeasureTheory.integral_const_mul]; congr; ext t    by_cases n_ne_zero : n = 0    · simp [n_ne_zero]    rw [mul_div_assoc, mul_assoc]    congr    rw [(div_eq_iff ?_).mpr]    · have := @mul_cpow_ofReal_nonneg (a := X / (n : ℝ)) (b := (n : ℝ)) (r := σ + I * t) ?_ ?_      · push_cast at this ⊢        rw [← this, div_mul_cancel₀]        · simp only [ne_eq, Nat.cast_eq_zero, n_ne_zero, not_false_eq_true]      · apply div_nonneg (by linarith : 0 ≤ X); simp      · simp    · simp only [ne_eq, cpow_eq_zero_iff, Nat.cast_eq_zero, n_ne_zero, false_and,        not_false_eq_true]  · conv => rw [← mul_assoc, div_mul]; lhs; lhs; rhs; simp  · simp_rw [← tsum_mul_left, ← mul_assoc, mul_comm]  · have ht (t : ℝ) : -(σ + t * I) = (-1) * (σ + t * I) := by simp    have hn (n : ℂ) : (n / X) ^ (-1 : ℂ) = X / n := by simp [cpow_neg_one]    have (n : ℕ) : (log ((n : ℂ) / (X : ℂ)) * -1).im = 0 := by      simp [Complex.log_im, arg_eq_zero_iff, div_nonneg (Nat.cast_nonneg _) (by linarith : 0 ≤ X)]    have h (n : ℕ) (t : ℝ) : ((n : ℂ) / X) ^ ((-1 : ℂ) * (σ + t * I)) =        ((n / X) ^ (-1 : ℂ)) ^ (σ + ↑t * I) := by      rw [cpow_mul] <;> {rw [this n]; simp [Real.pi_pos, Real.pi_nonneg]}    conv => rhs; lhs; intro n; rhs; rhs; rhs; intro t; rhs; rw [ht t, h n t]; lhs; rw [hn]  · push_cast    congr    ext n    by_cases n_zero : n = 0    · simp [n_zero]    have n_pos : 0 < n := by      simpa only [n_zero, gt_iff_lt, false_or] using (Nat.eq_zero_or_pos n)    congr    have := mellinInv_mellin_eq σ (f := fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) (x := n / X)      ?_ ?_ ?_ ?_    · beta_reduce at this      dsimp [mellinInv, VerticalIntegral] at this      convert! this using 4      · norm_cast      · rw [mul_comm]        norm_cast    · exact div_pos (by exact_mod_cast n_pos) (by linarith : 0 < X)    · apply Smooth1MellinConvergent diffSmoothingF suppSmoothingF ⟨εpos, ε_lt_one⟩        SmoothingFpos mass_one      simp only [ofReal_re]      linarith    · dsimp [VerticalIntegrable]      apply SmoothedChebyshevDirichlet_aux_integrable diffSmoothingF SmoothingFpos        suppSmoothingF mass_one εpos ε_lt_one σ_gt σ_le    · refine ContinuousAt.comp (g := ofReal) RCLike.continuous_ofReal.continuousAt ?_      exact Smooth1ContinuousAt diffSmoothingF SmoothingFpos suppSmoothingF        εpos (by positivity)