English
If f ≥ 0 and f ≤ g termwise, and there exists i with f(i) < g(i), and g is summable, then ∑' n f(n) < ∑' n g(n).
Русский
Пусть f ≥ 0 и f ≤ g покомпонентно, существует i с f(i) < g(i), и g суммируема. Тогда ∑ f(n) < ∑ g(n).
LaTeX
$$$\left(\forall i, f(i) \ge 0\right) \land \left(\forall i, f(i) \le g(i)\right) \land \left(\exists i, f(i) < g(i)\right) \land \text{Summable } g \Rightarrow \sum' n, f(n) < \sum' n, g(n)$$$
Lean4
/-- 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`. -/
protected theorem tsum_lt_tsum_of_nonneg {i : ℕ} {f g : ℕ → ℝ} (h0 : ∀ b : ℕ, 0 ≤ f b) (h : ∀ b : ℕ, f b ≤ g b)
(hi : f i < g i) (hg : Summable g) : ∑' n, f n < ∑' n, g n :=
Summable.tsum_lt_tsum h hi (.of_nonneg_of_le h0 h hg) hg
