norm_prime_cpow_le_one_half — Mathlib

English

For a prime p and s with Re(s) > 1, the norm of p^(-s) is at most 1/2.

Русский

Для простого p и s с Re(s) > 1 нормa p^(-s) не превосходит 1/2.

LaTeX

$$Let p be a prime and s ∈ ℂ with Re(s) > 1. ‖p^(-s)‖ ≤ 1/2.$$

Lean4

theorem norm_prime_cpow_le_one_half (p : Nat.Primes) {s : ℂ} (hs : 1 < s.re) : ‖(p : ℂ) ^ (-s)‖ ≤ 1 / 2 :=
  by
  rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]
  refine
    (Real.rpow_le_rpow_of_nonpos zero_lt_two (Nat.cast_le.mpr p.prop.two_le) <| by rw [neg_re];
          linarith only [hs]).trans
      ?_
  rw [one_div, ← Real.rpow_neg_one]
  exact Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

Похожие утверждения