Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.norm_one_sub_cpow_neg_vertical_le

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:99 to 107

Source documentation

On the vertical line σ + it, ‖1 - p^{-s}‖ ≤ 1 + p^{-σ}.

Exact Lean statement

lemma norm_one_sub_cpow_neg_vertical_le (p : Nat.Primes) (σ t : ℝ) :
    ‖(1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t))‖ ≤ 1 + ((p : ℕ) : ℝ) ^ (-σ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_one_sub_cpow_neg_vertical_le (p : Nat.Primes) (σ t : ℝ) :    ‖(1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t))‖ ≤ 1 + ((p : ℕ) : ℝ) ^ (-σ) := by  set s := verticalLine σ t  have hre : s.re = σ := verticalLine_re σ t  calc    ‖1 - ((p : ℕ) : ℂ) ^ (-s)‖ ≤ 1 + ‖((p : ℕ) : ℂ) ^ (-s)‖ := by      simpa [sub_eq_add_neg, norm_one, norm_neg] using        norm_add_le (1 : ℂ) (-((p : ℕ) : ℂ) ^ (-s))    _ = 1 + ((p : ℕ) : ℝ) ^ (-σ) := by rw [norm_cpow_neg_eq_rpow_neg_re, hre]