Kadiri.identity_16

@[blueprint  "kadiri-identity-16"  (title := "Equation (16) of \\cite{Kadiri2005}: intermediate identity")  (statement := /-- Under the hypotheses of \ref{kadiri-prop-2-1}: for every  $s \in \mathbb{C}$ with $\Re s > 1$,  $$ \Re \sum_{n \geq 1} \frac{\Lambda(n)}{n^s} f(\log n)   = f(0) \Bigl( \Re \Bigl( \sum_{n \geq 1} \frac{\Lambda(n)}{n^s} - \frac{1}{s - 1}                  + \sum_{\rho \in Z(\zeta)} \Bigl( \frac{1}{\rho} + \frac{1}{s - \rho} \Bigr) \Bigr)                  - \sum_{\rho \in Z(\zeta)} \Re \frac{1}{\rho} \Bigr)   + \Re F(s - 1) - \sum_{\rho \in Z(\zeta)} \Re F(s - \rho)   + \Re \Bigl( \frac{1}{2\pi i} \int_{1/2 - i\infty}^{1/2 + i\infty}       \Re \tfrac{\Gamma'}{\Gamma}\!\left(\tfrac{z}{2}\right) \frac{F_2(s - z)}{(s - z)^2}\, dz       + \frac{F_2(s)}{s^2} \Bigr). $$  This is the real-part form of \ref{kadiri-identity-16-complex}; the substantive  derivation from \ref{kadiri-thm-3-1-q1} via the Kadiri test function  $\varphi(y) = (f(0) - f(y)) e^{-y s} \mathbf{1}_{y \geq 0}$ lives in that sublemma.  The zero contribution in the $f(0)$-coefficient uses the absolutely convergent  Hadamard-paired block $\sum_\rho (1/\rho + 1/(s - \rho))$ together with the absolutely  convergent real correction $\sum_\rho \Re(1/\rho)$, matching  \ref{kadiri-hadamard-identity}; the standalone $\sum_\rho 1/(s - \rho)$ does not  converge unconditionally. The restriction $\Re s > 1$ is where the Dirichlet series for  $-\zeta'/\zeta(s)$ converges absolutely; this is also the range used in Kadiri's  downstream zero-free region argument, so we do not extend further. -/)  (proof := /-- Apply \ref{kadiri-identity-16-complex} to obtain the $\mathbb{C}$-valued  equation, then take real parts of both sides. The grouped zero sum is absolutely  summable (each summand is $-F_2(s-\rho)/(s-\rho)^2$ by \ref{kadiri-laplace-ibp}), so  $\Re$ passes through it; each term splits as $f(0) \Re(1/(s-\rho)) - \Re F(s-\rho)$,  and both real families are absolutely summable. Regrouping  $\sum_\rho \Re(1/(s-\rho))$ into the paired block minus the $\Re(1/\rho)$ correction  is legitimate by the paired-family summability. -/)  (latexEnv := "lemma")  (discussion := 1488)]theorem identity_16 {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)    {s : ℂ} (hs : 1 < s.re) :    (∑' n : ℕ, (Λ n : ℂ) / (n : ℂ) ^ s * ((f (Real.log n) : ℝ) : ℂ)).re =      f 0 * (((∑' n : ℕ, (Λ n : ℂ) / (n : ℂ) ^ s) - 1 / (s - 1) +                ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),                  (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re -              ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),                (1 / (ρ.val : ℂ)).re)        + (laplaceTransform f (s - 1)).re        - ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) .univ,            (laplaceTransform f (s - ρ.val)).re        + ((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 := by  have hcomplex := identity_16_complex hd hf_C2 hf_supp hf_d hf_deriv_0 hf_deriv_d    hf_deriv2_d hs  have hsub := summable_lap_sub_pole_at_zeros hd hf_C2 hf_supp hf_d hf_deriv_0    hf_deriv_d s  have hre1 := summable_re_one_div_at_zeros s  have hreF := summable_lap_re_at_zeros hd hf_nonneg hf_C2 hf_supp hf_d hf_deriv_0    hf_deriv_d hf_deriv2_d s  -- `Re` commutes with the grouped zero sum, which is genuinely summable  have htsum_re :      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),          ((f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val))).re =      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),          ((f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val)).re := by    simpa using ContinuousLinearMap.map_tsum Complex.reCLM hsub  -- pointwise real part of the grouped summand  have hpt : ∀ ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),      ((f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val)).re =        f 0 * (1 / (s - ρ.val)).re - (laplaceTransform f (s - ρ.val)).re := by    intro ρ    have hmul : ((f 0 : ℝ) : ℂ) / (s - ρ.val) =        ((f 0 : ℝ) : ℂ) * (1 / (s - ρ.val)) := div_eq_mul_one_div _ _    rw [Complex.sub_re, hmul, Complex.re_ofReal_mul]  -- split the real tsum of differences  have hsplit :      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),          (f 0 * (1 / (s - ρ.val)).re - (laplaceTransform f (s - ρ.val)).re)) =      f 0 * (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),          (1 / (s - ρ.val)).re) -        ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),          (laplaceTransform f (s - ρ.val)).re := by    rw [Summable.tsum_sub (hre1.mul_left (f 0)) hreF, tsum_mul_left]  rw [hcomplex]  simp only [Complex.add_re, Complex.sub_re]  rw [htsum_re, tsum_congr hpt, hsplit, Complex.re_ofReal_mul, Complex.sub_re,    re_shifted_sum_eq_paired_sub_re_inv s]  ring