Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.riemannZeta_order_pos_positiveHeightZero

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:229 to 249

Mathematical statement

Exact Lean statement

lemma riemannZeta_order_pos_positiveHeightZero {T : ℝ}
    (rho : riemannZeta.zeroes_rect (.univ : Set ℝ) (.Ioo 0 T)) :
    0 < riemannZeta.order (rho : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma riemannZeta_order_pos_positiveHeightZero {T : ℝ}    (rho : riemannZeta.zeroes_rect (.univ : Set ℝ) (.Ioo 0 T)) :    0 < riemannZeta.order (rho : ℂ) := by  have han := riemannZeta_analyticAt_positiveHeightZero rho  have hzero := riemannZeta_positiveHeightZero_zero rho  have horder_ne_top := riemannZeta_meromorphicOrderAt_ne_top_positiveHeightZero rho  have hanOrder_ne_zero : analyticOrderAt riemannZeta (rho : ℂ) ≠ 0 := by    intro h    exact (han.analyticOrderAt_eq_zero.mp h) hzero  unfold riemannZeta.order  cases hO : analyticOrderAt riemannZeta (rho : ℂ) with  | top =>      exfalso      exact horder_ne_top (by simp [han.meromorphicOrderAt_eq, hO])  | coe n =>      have hn_pos : 0 < n := by        exact Nat.pos_of_ne_zero (by          intro hn          exact hanOrder_ne_zero (by simp [hO, hn]))      rw [han.meromorphicOrderAt_eq, hO, ENat.map_coe, WithTop.untopD_coe]      exact_mod_cast hn_pos