Kadiri.summable_lap_re_at_zeros

@[blueprint  "kadiri-summable-lap-at-zeros"  (title := "Summability of $\\sum_\\rho \\Re F(s - \\rho)$")  (statement := /-- Under the hypotheses of \ref{kadiri-prop-2-1}, the sum  $\sum_{\rho \in Z(\zeta)} \Re F(s - \rho)$ over the non-trivial zeros of $\zeta$ is  convergent (Lean: `Summable`). -/)  (proof := /-- Combine \ref{kadiri-laplace-re-decay} (giving $|\Re F(s-\rho)| \leq  C/|\Im(s-\rho)|^2 = C/(\Im s - \gamma)^2$ for $|\gamma|$ large, since the real part  $\Re(s-\rho) = \Re s - \beta$ stays in the bounded strip $[\Re s - 1, \Re s]$) with  the unconditional crude counting bound $N(T) = O(T^{3/2})$ proved in  the Backlund zero-count module: over the dyadic shells  $|\gamma| \in [2^k, 2^{k+1})$ the shell count is $O(3^k)$ while each term is at  most $4^{-k}$, so $\sum_{|\gamma| \geq 1} 1/|\gamma|^2 < \infty$. The finitely many  small-$|\gamma|$ terms are absorbed by cofiniteness. The sharper  \ref{kadiri-backlund-bound} route ($N(T) \ll T \log T$) is not needed here and  remains the path to the explicit numerics. -/)  (latexEnv := "lemma")  (discussion := 1477)]theorem summable_lap_re_at_zeros {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 : ℂ) :    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦                (laplaceTransform f (s - ρ.val)).re) := by  obtain ⟨C, hC⟩ := laplaceTransform_re_decay hd hf_nonneg hf_C2 hf_supp hf_d    hf_deriv_0 hf_deriv_d hf_deriv2_d (s.re - 1) s.re  have htail : Summable (fun ρ : NontrivialZeros ↦      C * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))) :=    (summable_zeroImagSquareTail_shifted_unconditional s).mul_left C  refine Summable.of_norm_bounded_eventually htail ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset (nontrivialZeros_shifted_abs_im_lt_one_finite s)  intro ρ hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have him : 1 ≤ |(s - (ρ : ℂ)).im| := le_of_not_gt hsmall  have hre : (ρ : ℂ).re ∈ Set.Ioo (0 : ℝ) 1 := ρ.property.1  have hre_lo : s.re - 1 ≤ (s - (ρ : ℂ)).re := by    rw [Complex.sub_re]    linarith [hre.2]  have hre_hi : (s - (ρ : ℂ)).re ≤ s.re := by    rw [Complex.sub_re]    linarith [hre.1]  have hdecay := hC (s - (ρ : ℂ)) hre_lo hre_hi him  apply hbad  rw [Real.norm_eq_abs]  calc |(laplaceTransform f (s - (ρ : ℂ))).re|      ≤ C / (s - (ρ : ℂ)).im ^ 2 := hdecay    _ = C * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) := by        rw [inv_pow, sq_abs, div_eq_mul_inv]