Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zeroSquareTailSummable_shift_of_zero

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:706 to 720

Source documentation

Shifted square zero tails follow from the unshifted square zero tail.

Exact Lean statement

theorem zeroSquareTailSummable_shift_of_zero {s : ℂ}
    (htail0 : zeroSquareTailSummable 0) :
    zeroSquareTailSummable s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zeroSquareTailSummable_shift_of_zero {s : ℂ}    (htail0 : zeroSquareTailSummable 0) :    zeroSquareTailSummable s := by  unfold zeroSquareTailSummable at htail0 ⊢  refine Summable.of_norm_bounded_eventually (htail0.mul_left 4) ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset (nontrivialZeros_norm_lt_finite (2 * ‖s‖))  intro rho hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have hlarge : 2 * ‖s‖ ≤ ‖(rho : ℂ)‖ := le_of_not_gt hsmall  have hle := zeroSquareTail_shift_le_four_zero (s := s) (rho := rho) hlarge  have hnorm : ‖zeroSquareTail s rho‖ = zeroSquareTail s rho := by    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]  exact hbad (by simpa [hnorm] using hle)