Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zeroSquareTailSummable_of_imag_tail

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:736 to 751

Source documentation

The unshifted norm-square zero tail follows from the height-square zero tail.

Exact Lean statement

theorem zeroSquareTailSummable_of_imag_tail
    (him : zeroImagSquareTailSummable) :
    zeroSquareTailSummable 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zeroSquareTailSummable_of_imag_tail    (him : zeroImagSquareTailSummable) :    zeroSquareTailSummable 0 := by  unfold zeroImagSquareTailSummable at him  unfold zeroSquareTailSummable  refine Summable.of_norm_bounded_eventually him ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset nontrivialZeros_abs_im_lt_one_finite  intro rho hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have hlarge : 1 ≤ |(rho : ℂ).im| := le_of_not_gt hsmall  have hle := zeroSquareTail_le_imagSquareTail_of_large_im (rho := rho) hlarge  have hnorm : ‖zeroSquareTail 0 rho‖ = zeroSquareTail 0 rho := by    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]  exact hbad (by simpa [hnorm] using hle)