Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroes_rect_Ioo_critical_positive_height_finite

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:136 to 147

Mathematical statement

Exact Lean statement

lemma zeroes_rect_Ioo_critical_positive_height_finite (T : ℝ) :
    (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroes_rect_Ioo_critical_positive_height_finite (T : ℝ) :    (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)).Finite := by  rw [riemannZeta.zeroes_rect_eq]  let S : Set ℂ := (Complex.re ⁻¹' Set.Icc (0 : ℝ) 1) ∩    (Complex.im ⁻¹' Set.Icc (0 : ℝ) T)  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, Set.Ioo_subset_Icc_self him⟩, hzeta⟩