Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.summable_lap_sub_pole_at_zeros

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2911 to 2945

Source documentation

Unconditional summability over the non-trivial zeros of the pole-subtracted Laplace transform. The un-subtracted complex sum ∑ ρ, F(s - ρ) is not absolutely summable when f 0 ≠ 0 (terms of norm ~ |f 0| / |Im ρ|); in equation (16) the groups f 0 * ∑ ρ, 1/(s - ρ) and -∑ ρ, F(s - ρ) combine into exactly this summand, which is O(1/(Im ρ)^2) and summable against the crude counting majorant.

Exact Lean statement

theorem summable_lap_sub_pole_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 : ℂ) :
    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦
      (f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.val))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem summable_lap_sub_pole_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 : ℂ) :    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦      (f 0 : ℂ) / (s - ρ.val) - laplaceTransform f (s - ρ.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 : 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 him0 : (s - (ρ : ℂ)).im ≠ 0 := by    intro h    rw [h] at him    norm_num at him  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 hdecay := hC (s - (ρ : ℂ)) hre_lo him0  apply hbad  calc ‖(f 0 : ℂ) / (s - (ρ : ℂ)) - laplaceTransform f (s - (ρ : ℂ))‖      ≤ C / (s - (ρ : ℂ)).im ^ 2 := hdecay    _ = C * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) := by        rw [inv_pow, sq_abs, div_eq_mul_inv]