Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.riemannZeta_order_pos_nontrivialZero

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:90 to 109

Mathematical statement

Exact Lean statement

lemma riemannZeta_order_pos_nontrivialZero (rho : NontrivialZeros) :
    0 < riemannZeta.order (rho : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma riemannZeta_order_pos_nontrivialZero (rho : NontrivialZeros) :    0 < riemannZeta.order (rho : ℂ) := by  have han := riemannZeta_analyticAt_nontrivialZero rho  have hzero := riemannZeta_nontrivialZero_zero rho  have horder_ne_top := riemannZeta_meromorphicOrderAt_ne_top_nontrivialZero 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