Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.positiveHeightZero_re_mem_Ioo

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:325 to 338

Mathematical statement

Exact Lean statement

lemma positiveHeightZero_re_mem_Ioo {T : ℝ}
    (rho : riemannZeta.zeroes_rect (.univ : Set ℝ) (.Ioo 0 T)) :
    (rho : ℂ).re ∈ Set.Ioo (0 : ℝ) 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma positiveHeightZero_re_mem_Ioo {T : ℝ}    (rho : riemannZeta.zeroes_rect (.univ : Set ℝ) (.Ioo 0 T)) :    (rho : ℂ).re ∈ Set.Ioo (0 : ℝ) 1 := by  have him_pos : 0 < (rho : ℂ).im := rho.property.2.1.1  have hzeta : riemannZeta (rho : ℂ) = 0 := rho.property.2.2  have hnot_re_nonpos : ¬ (rho : ℂ).re ≤ 0 := by    intro hre    exact (riemannZeta_ne_zero_of_re_nonpos_im_ne_zero hre him_pos.ne') hzeta  have hre_pos : 0 < (rho : ℂ).re := lt_of_not_ge hnot_re_nonpos  have hnot_re_one_le : ¬ 1 ≤ (rho : ℂ).re := by    intro hre    exact (riemannZeta_ne_zero_of_one_le_re hre) hzeta  have hre_lt_one : (rho : ℂ).re < 1 := lt_of_not_ge hnot_re_one_le  exact ⟨hre_pos, hre_lt_one⟩