Kadiri.eq_5

@[blueprint  "kadiri-eq-5"  (title := "Damped explicit formula (Kadiri 2005, eq.~(5))")  (statement := /-- For $f$ as in \ref{kadiri-prop-2-1}, real parameters $\kappa, \delta$, and  $s \in \mathbb{C}$, set  $$ \Delta_1(s) := T_1(s) - \kappa T_1(s + \delta), \qquad     \Delta_2(s) := T_2(s) - \kappa T_2(s + \delta), \qquad     D(s) := \Re F(s) - \kappa \Re F(s + \delta), $$  where $T_1, T_2$ are the "gamma" and "remainder" contributions to the RHS of  \ref{kadiri-prop-2-1}. Then  $$ \Re \sum_{n \geq 1} \frac{\Lambda(n)}{n^s} f(\log n) \left( 1 - \frac{\kappa}{n^\delta} \right)       = f(0) \Delta_1(s) + D(s - 1) - \sum_{\rho \in Z(\zeta)} D(s - \rho) + \Delta_2(s). $$  -/)  (proof := /-- Direct substitution: apply \ref{kadiri-prop-2-1} at $s$ and at $s + \delta$,  multiply the latter by $\kappa$, subtract, and use the identity  $n^{-s} - \kappa n^{-(s + \delta)} = n^{-s} (1 - \kappa n^{-\delta})$ to combine the LHS,  while the definitions of $\Delta_1, \Delta_2, D$ combine the corresponding RHS terms. -/)  (latexEnv := "lemma")]theorem eq_5 {d : ℝ} (hd : 0 < d) {f : ℝ → ℝ} (hf_nonneg : ∀ t, 0 ≤ f t)    (hf_C2 : ContDiffOn ℝ 2 f (.Icc 0 d)) (hf_supp : tsupport f ⊆ .Ico 0 d)    (hf_d : f d = 0) (hf_deriv_0 : derivWithin f (Set.Icc 0 d) 0 = 0) (hf_deriv_d : derivWithin f (Set.Icc 0 d) d = 0)    (hf_deriv2_d : derivWithin (fun x => derivWithin f (Set.Icc 0 d) x) (Set.Icc 0 d) d = 0) (κ : ℝ) {δ : ℝ} (hδ : 0 ≤ δ)    {s : ℂ} (hs : 1 < s.re) :    (∑' n : ℕ, Λ n / n ^ s * f (Real.log n) * ((1 : ℂ) - κ / n ^ (δ : ℂ))).re =      f 0 * Δ1 κ δ s + D f κ δ (s - 1)        - ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) .univ, D f κ δ (s - ρ.val) + Δ2 f κ δ s := by  have hsδ : 1 < (s + δ).re := by    simp only [Complex.add_re, Complex.ofReal_re]; linarith  have h1 := prop_2_1 hd hf_nonneg hf_C2 hf_supp hf_d hf_deriv_0 hf_deriv_d hf_deriv2_d hs  have h2 := prop_2_1 hd hf_nonneg hf_C2 hf_supp hf_d hf_deriv_0 hf_deriv_d hf_deriv2_d hsδ  have hLHS :      (∑' n : ℕ, Λ n / n ^ s * f (Real.log n) * ((1 : ℂ) - κ / n ^ (δ : ℂ))).re =      (∑' n : ℕ, Λ n / (n : ℂ) ^ s * f (Real.log n)).re        - κ * (∑' n : ℕ, Λ n / (n : ℂ) ^ (s + δ) * f (Real.log n)).re := by    have hpoint (n : ℕ) :        Λ n / n ^ s * f (Real.log n) * ((1 : ℂ) - κ / n ^ (δ : ℂ)) =        Λ n / n ^ s * f (Real.log n) - κ * (Λ n / n ^ (s + δ) * f (Real.log n)) := by      rcases eq_or_ne n 0 with rfl | hn      · simp      · rw [cpow_add s (δ : ℂ) (Nat.cast_ne_zero.mpr hn)]        field_simp    have h_complex :        (∑' n : ℕ, Λ n / n ^ s * f (Real.log n) * ((1 : ℂ) - κ / n ^ (δ : ℂ))) =        (∑' n : ℕ, Λ n / (n : ℂ) ^ s * f (Real.log n)) -        (κ : ℂ) * (∑' n : ℕ, Λ n/ (n : ℂ) ^ (s + δ) * f (Real.log n)) := by      simp_rw [hpoint]      rw [((summable_f_log hf_supp _).hasSum.sub ((summable_f_log hf_supp _).mul_left        (κ : ℂ)).hasSum).tsum_eq, tsum_mul_left]    rw [h_complex, Complex.sub_re, Complex.re_ofReal_mul]  have hZeros :      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) .univ, D f κ δ (s - ρ.val)) =      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) .univ,          (laplaceTransform f (s - ρ.val)).re)        - κ * (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) .univ,                 (laplaceTransform f ((s + δ) - ρ.val)).re) := by    have harg : ∀ ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (s - ρ.val) + δ = s + δ - ρ.val := fun _ ↦ by ring    simp_rw [D, harg, (h1.1.hasSum.sub (h2.1.mul_left κ).hasSum).tsum_eq, tsum_mul_left]  have hT1s : -(1 / 2 : ℝ) * Real.log Real.pi +      (1 / 2 : ℝ) * (digamma (s / 2 + 1)).re = T1 s := rfl  have hT1sd : -(1 / 2 : ℝ) * Real.log Real.pi +      (1 / 2 : ℝ) * (digamma ((s + (δ : ℂ)) / 2 + 1)).re = T1 (s + (δ : ℂ)) := rfl  have hT2s : ((1 / (2 * (Real.pi : ℂ))) *      (∫ t : ℝ,        ((digamma ((1 / 2 + (t : ℂ) * I) / 2)).re : ℂ) *          laplaceTransform (fun u ↦ deriv (deriv f) u) (s - (1 / 2 + (t : ℂ) * I))          / (s - (1 / 2 + (t : ℂ) * I)) ^ 2)      + laplaceTransform (fun u ↦ deriv (deriv f) u) s / s ^ 2).re = T2 f s := rfl  have hT2sd : ((1 / (2 * (Real.pi : ℂ))) *      (∫ t : ℝ,        ((digamma ((1 / 2 + (t : ℂ) * I) / 2)).re : ℂ) *          laplaceTransform (fun u ↦ deriv (deriv f) u) (s + (δ : ℂ) - (1 / 2 + (t : ℂ) * I))          / (s + (δ : ℂ) - (1 / 2 + (t : ℂ) * I)) ^ 2)      + laplaceTransform (fun u ↦ deriv (deriv f) u) (s + (δ : ℂ)) / (s + (δ : ℂ)) ^ 2).re =      T2 f (s + (δ : ℂ)) := rfl  rw [hLHS, h1.2, h2.2, hZeros, hT1s, hT1sd, hT2s, hT2sd]  simp only [Δ1, Δ2, D]  ring_nf