enorm_le_of_bounded — Mathlib

English

If the NN-norms of f(i) are bounded by a summable NNReal sequence g(i), then f is summable.

Русский

Если nnnorm(f(i)) ≤ g(i) в nnreal и ∑ g(i) сходится, то ∑ f(i) сходится.

LaTeX

$$$\\text{Summable } g \\Rightarrow \\left( \\forall i, \\|f(i)\\|_+ \\le g(i) \\Rightarrow \\text{Summable } f \\right)$$$

Lean4

theorem enorm_le_of_bounded {f : ι → ε} {g : ι → ℝ≥0∞} {a : ε} {b : ℝ≥0∞} (hf : HasSum f a) (hg : HasSum g b)
    (h : ∀ i, ‖f i‖ₑ ≤ g i) : ‖a‖ₑ ≤ b := by
  exact le_of_tendsto_of_tendsto' hf.enorm hg fun _s ↦ enorm_sum_le_of_le _ fun i _hi ↦ h i

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