Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.norm_cpow_neg_lt_one

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:58 to 67

Source documentation

For a prime p and s with real part > 1, ‖p^{-s}‖ < 1.

Exact Lean statement

lemma norm_cpow_neg_lt_one (p : Nat.Primes) (s : ℂ) (hs : 1 < s.re) :
    ‖((p : ℕ) : ℂ) ^ (-s)‖ < 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_cpow_neg_lt_one (p : Nat.Primes) (s : ℂ) (hs : 1 < s.re) :    ‖((p : ℕ) : ℂ) ^ (-s)‖ < 1 := by  have hx1 : 1 < ((p : ℕ) : ℝ) := by    have h2 : (2 : ℝ) ≤ ((p : ℕ) : ℝ) := by exact_mod_cast (p.2.two_le : 2 ≤ (p : ℕ))    exact lt_of_lt_of_le one_lt_two h2  have hx0 : 0 < ((p : ℕ) : ℝ) := lt_trans zero_lt_one hx1  have hnorm : ‖((p : ℕ) : ℂ) ^ (-s)‖ = ((p : ℕ) : ℝ) ^ (-s.re) :=    Complex.norm_cpow_eq_rpow_re_of_pos hx0 (-s)  have hz : -s.re < 0 := neg_lt_zero.mpr (lt_trans zero_lt_one hs)  simpa [hnorm] using Real.rpow_lt_one_of_one_lt_of_neg hx1 hz