Kadiri.summable_kadiriTestFn_weighted_at_zeros

theorem summable_kadiriTestFn_weighted_at_zeros {d : ℝ} (hd : 0 < d) {f : ℝ → ℝ}    (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)    {s : ℂ} (hs : 1 < s.re) :    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦      (∫ y, kadiriTestFn f s y * exp (ρ.val * (y : ℂ)) ∂volume) *        (riemannZeta.order ρ.val : ℂ)) := by  have hpt : ∀ ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),      (∫ y, kadiriTestFn f s y * exp (ρ.val * (y : ℂ)) ∂volume) =      (f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val) := by    intro ρ    have hre : (0 : ℝ) < (s + -ρ.val).re := by      have hlt : (ρ.val).re < 1 := ρ.property.1.2      simp only [Complex.add_re, Complex.neg_re]      linarith    have h := kadiriTestFn_laplaceTransform hd hf_C2 hf_supp s (-ρ.val) hre    simp only [neg_neg] at h    rw [h, show s + -ρ.val = s - ρ.val by ring]  have hmain : Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦      ((f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val)) *        (riemannZeta.order ρ.val : ℂ)) := by    obtain ⟨C, hC⟩ := laplaceTransform_sub_pole_norm_decay hd hf_C2 hf_supp hf_d      hf_deriv_0 hf_deriv_d (s.re - 1)    have htail := (weighted_zeroImagSquareTail_shifted_summable 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 him0 : (s - (ρ : ℂ)).im ≠ 0 := by      intro h      rw [h] at him      norm_num at him    have hre_lo : s.re - 1 ≤ (s - (ρ : ℂ)).re := by      rw [Complex.sub_re]      linarith [ρ.property.1.2]    have hdecay := hC (s - (ρ : ℂ)) hre_lo him0    apply hbad    have hordZ : (0 : ℤ) ≤ riemannZeta.order (ρ : ℂ) :=      riemannZeta_order_nonneg (nontrivialZero_ne_one ρ)    have hord : (0 : ℝ) ≤ ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) := by      exact_mod_cast hordZ    rw [norm_mul]    have hnormord : ‖((riemannZeta.order (ρ : ℂ) : ℤ) : ℂ)‖ =        ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) := by      rw [Complex.norm_intCast]      exact_mod_cast abs_of_nonneg hordZ    rw [hnormord]    calc ‖(f 0 : ℂ) / (s - (ρ : ℂ)) - laplaceTransform f (s - (ρ : ℂ))‖ *          ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ)        ≤ (C / (s - (ρ : ℂ)).im ^ 2) * ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) :=          mul_le_mul_of_nonneg_right hdecay hord      _ = C * (((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) *            (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))) := by          rw [inv_pow, sq_abs, div_eq_mul_inv]          ring  exact hmain.congr fun ρ ↦ by rw [hpt ρ]