Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.summable_zeroImagSquareTail_shifted

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1702 to 1716

Source documentation

The shifted height-square tail is summable once the unshifted height-square tail is.

Exact Lean statement

theorem summable_zeroImagSquareTail_shifted
    (him : zeroImagSquareTailSummable) (s : ℂ) :
    Summable (fun rho : NontrivialZeros ↦ |(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem summable_zeroImagSquareTail_shifted    (him : zeroImagSquareTailSummable) (s : ℂ) :    Summable (fun rho : NontrivialZeros ↦ |(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ)) := by  unfold zeroImagSquareTailSummable at him  refine Summable.of_norm_bounded_eventually (him.mul_left 4) ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset (nontrivialZeros_abs_im_lt_finite (2 * |s.im| + 2))  intro rho hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have hlarge : 2 * |s.im| + 2 ≤ |(rho : ℂ).im| := le_of_not_gt hsmall  have hle := zeroImagSquareTail_shifted_le_four (s := s) (rho := rho) hlarge  have hnorm : ‖|(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ)‖ = |(s - (rho : ℂ)).im|⁻¹ ^ (2 : ℕ) := by    rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]  exact hbad (by simpa [hnorm] using hle)