Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.nontrivialZeros_abs_im_lt_finite

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:601 to 612

Source documentation

Only finitely many non-trivial zeros have bounded absolute height.

Exact Lean statement

lemma nontrivialZeros_abs_im_lt_finite (T : ℝ) :
    ({rho : NontrivialZeros | |(rho : ℂ).im| < T} : Set NontrivialZeros).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma nontrivialZeros_abs_im_lt_finite (T : ℝ) :    ({rho : NontrivialZeros | |(rho : ℂ).im| < T} : Set NontrivialZeros).Finite := by  apply Set.Finite.subset (nontrivialZeros_norm_lt_finite (T + 1))  intro rho hrho  rw [Set.mem_setOf_eq] at hrho ⊢  have hre_nonneg : 0 ≤ (rho : ℂ).re := le_of_lt rho.property.1.1  have hre_abs_lt_one : |(rho : ℂ).re| < 1 := by    rw [abs_of_nonneg hre_nonneg]    exact rho.property.1.2  have hnorm_le : ‖(rho : ℂ)‖ ≤ |(rho : ℂ).re| + |(rho : ℂ).im| :=    Complex.norm_le_abs_re_add_abs_im (rho : ℂ)  linarith