Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroes_rect_Ioo_critical_zero_height_finite

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:386 to 397

Mathematical statement

Exact Lean statement

lemma zeroes_rect_Ioo_critical_zero_height_finite :
    (riemannZeta.zeroes_rect (.Ioo (0 : ℝ) 1) (.Icc 0 0)).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroes_rect_Ioo_critical_zero_height_finite :    (riemannZeta.zeroes_rect (.Ioo (0 : ℝ) 1) (.Icc 0 0)).Finite := by  rw [riemannZeta.zeroes_rect_eq]  let S : Set ℂ := (Complex.re ⁻¹' Set.Icc (0 : ℝ) 1) ∩    (Complex.im ⁻¹' Set.Icc (0 : ℝ) 0)  have hS : IsCompact S := by    exact Complex.equivRealProdCLM.toHomeomorph.isClosedEmbedding.isCompact_preimage      (isCompact_Icc.prod isCompact_Icc)  refine (riemannZeta.zeroes_on_Compact_finite' (S := S) hS).subset ?_  intro z hz  rcases hz with ⟨⟨hre, him⟩, hzeta⟩  exact ⟨⟨Set.Ioo_subset_Icc_self hre, him⟩, hzeta⟩