of_re_le_re — Mathlib

English

If Re(s) ≤ Re(s'), then LSeriesSummable f s → LSeriesSummable f s'.

Русский

Если Re(s) ≤ Re(s'), то суммируемость L-серии f в s) ведёт к суммируемости в s'.

LaTeX

$$(s.re ≤ s'.re) → (LSeriesSummable(f,s) → LSeriesSummable(f,s'))$$

Lean4

theorem of_re_le_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re ≤ s'.re) (hf : LSeriesSummable f s) : LSeriesSummable f s' :=
  by
  rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
  exact hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (norm_term_le_of_re_le_re f h)

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