tsum_comp_le_tsum_of_inj — Mathlib

English

If f: α → ℝ≥0 is summable and i: β → α is injective, then ∑ f(i x) ≤ ∑ f(x).

Русский

Если f: α → ℝ≥0 суммируема и i: β → α инъективно, то сумма по композиции f ∘ i не превосходит суммарную по f.

LaTeX

$$$\\\\forall f : \\\\alpha \\\\to \\\\mathbb{R}_{\\\\ge 0}, \\\\mathrm{Summable}(f) \\\\Rightarrow \\\\forall i : \\\\beta \\\\to \\\\alpha, \\\\mathrm{Injective}(i) \\\\Rightarrow \\sum' x, f(i x) \\\\le \\sum' x, f x$$$

Lean4

theorem tsum_comp_le_tsum_of_inj {β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α} (hi : Function.Injective i) :
    (∑' x, f (i x)) ≤ ∑' x, f x :=
  (summable_comp_injective hf hi).tsum_le_tsum_of_inj i hi (fun _ _ => zero_le _) (fun _ => le_rfl) hf

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