norm_term_eq — Mathlib

English

The norm of the nth term satisfies ‖term f s n‖ = 0 if n = 0, otherwise ‖f n‖ / n^{Re(s)}.

Русский

Норма n-го элемента ряда удовлетворяет: ‖term f s n‖ = 0, если n = 0; иначе ‖f n‖ / n^{Re(s)}.

LaTeX

$$$\\|\\operatorname{term}(f,s,n)\\| = \\begin{cases}0, & n=0 \\\\ \\dfrac{\\|f(n)\\|}{n^{\\Re(s)}}, & n \\neq 0\\end{cases}$$$

Lean4

theorem norm_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / n ^ s.re :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · simp [hn, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]

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