norm_term_le_of_re_le_re — Mathlib

English

If Re(s) ≤ Re(s'), then ‖term f s' n‖ ≤ ‖term f s n‖ for all n.

Русский

Если Re(s) ≤ Re(s'), то для всех n выполняется ‖term f s' n‖ ≤ ‖term f s n‖.

LaTeX

$$$\\text{Re}(s) \\le \\text{Re}(s') \\Rightarrow \\|\\operatorname{term}(f,s',n)\\| \\le \\|\\operatorname{term}(f,s,n)\\|$$$

Lean4

theorem norm_term_le_of_re_le_re (f : ℕ → ℂ) {s s' : ℂ} (h : s.re ≤ s'.re) (n : ℕ) : ‖term f s' n‖ ≤ ‖term f s n‖ :=
  by
  simp only [norm_term_eq]
  split
  · next => rfl
  · next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

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