Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.nontrivialZeros_norm_lt_finite

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:574 to 584

Source documentation

Only finitely many non-trivial zeros lie in a bounded norm ball.

Exact Lean statement

lemma nontrivialZeros_norm_lt_finite (R : ℝ) :
    ({rho : NontrivialZeros | ‖(rho : ℂ)‖ < R} : Set NontrivialZeros).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma nontrivialZeros_norm_lt_finite (R : ℝ) :    ({rho : NontrivialZeros | ‖(rho : ℂ)‖ < R} : Set NontrivialZeros).Finite := by  refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.coe_injective)  apply Set.Finite.subset    (riemannZeta.zeroes_on_Compact_finite' (ProperSpace.isCompact_closedBall (0 : ℂ) R))  intro z hz  rcases hz with ⟨rho, hrho, rfl⟩  constructor  · rw [Metric.mem_closedBall, dist_zero_right]    exact le_of_lt hrho  · exact rho.property.2.2