tsum_strict_mono — Mathlib

English

If Summable g and f < g, then ∑' n, f n < ∑' n, g n.

Русский

Если сумма по g сходится и f меньше g по каждой точке, то суммирования по f меньше сумма по g.

LaTeX

$$$\\\\forall f,g : \\\\mathbb{N} \\\\rightarrow \\\\mathbb{R}_{\\\\ge 0}, \\\\mathrm{Summable}(g) \\\\Rightarrow \\\\mathrm{Pi.preorder}.lt f g \\\\Rightarrow \\\\mathrm{Summable}(f) \\\\Rightarrow \\\\mathrm{instPartialOrderNNReal}.lt (\\\\sum n, f n) (\\\\sum n, g n)$$$

Lean4

@[mono]
theorem tsum_strict_mono {f g : α → ℝ≥0} (hg : Summable g) (h : f < g) : ∑' n, f n < ∑' n, g n :=
  let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  tsum_lt_tsum hle hi hg

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