Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.nontrivialZeros_shifted_abs_im_lt_one_finite

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:630 to 650

Source documentation

Only finitely many non-trivial zeros have shifted height less than one.

Exact Lean statement

lemma nontrivialZeros_shifted_abs_im_lt_one_finite (s : ℂ) :
    ({rho : NontrivialZeros | |(s - (rho : ℂ)).im| < 1} :
      Set NontrivialZeros).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma nontrivialZeros_shifted_abs_im_lt_one_finite (s : ℂ) :    ({rho : NontrivialZeros | |(s - (rho : ℂ)).im| < 1} :      Set NontrivialZeros).Finite := by  apply Set.Finite.subset (nontrivialZeros_norm_lt_finite (|s.im| + 2))  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 him_eq : (rho : ℂ).im = s.im - (s - (rho : ℂ)).im := by    simp only [Complex.sub_im]    ring  have him_le : |(rho : ℂ).im| ≤ |s.im| + |(s - (rho : ℂ)).im| := by    rw [him_eq]    exact abs_sub s.im (s - (rho : ℂ)).im  have him_lt : |(rho : ℂ).im| < |s.im| + 1 := by    linarith  have hnorm_le : ‖(rho : ℂ)‖ ≤ |(rho : ℂ).re| + |(rho : ℂ).im| :=    Complex.norm_le_abs_re_add_abs_im (rho : ℂ)  linarith