Theorems · Theorem · sequences and series

Summable.tsum_lt_tsum_of_nonneg

∀ {i : ℕ} {f g : ℕ → ℝ},
  (∀ (b : ℕ), 0 ≤ f b) → (∀ (b : ℕ), f b ≤ g b) → f i < g i → Summable g → ∑' (n : ℕ), f n < ∑' (n : ℕ), g n

If a sequence f with non-negative terms is dominated by a sequence g with summable series and at least one term of f is strictly smaller than the corresponding term in g, then the series of f is strictly smaller than the series of g.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Real

Cited by

0 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound