Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.one_sub_cpow_neg_vertical_ne_zero

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:110 to 119

Source documentation

On the vertical line σ + it with 1 < σ, the Euler factor 1 - p^{-s} is nonzero.

Exact Lean statement

lemma one_sub_cpow_neg_vertical_ne_zero (p : Nat.Primes) (σ t : ℝ) (hσ : 1 < σ) :
    1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma one_sub_cpow_neg_vertical_ne_zero (p : Nat.Primes) (σ t : ℝ) (hσ : 1 < σ) :    1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t) ≠ 0 := by  intro h  set s := verticalLine σ t  have hs : 1 < s.re := by rw [verticalLine_re]; exact hσ  have hp_eq_one : ((p : ℕ) : ℂ) ^ (-s) = 1 := by    rw [sub_eq_zero] at h; exact h.symm  have h_abs_lt : ‖((p : ℕ) : ℂ) ^ (-s)‖ < 1 := norm_cpow_neg_lt_one p s hs  rw [hp_eq_one, show ‖(1 : ℂ)‖ = 1 from by simp] at h_abs_lt  exact lt_irrefl 1 h_abs_lt