English
For f: α → Real, if f is summable and hn ≥ 0, and i : β → α is injective, then tsum (f ∘ i) ≤ tsum f.
Русский
Для f: α → Real, если f суммируема и f(a) ≥ 0, и i: β → α инъективно, то сумма по f ∘ i не превосходит сумму по f.
LaTeX
$$$\\\\forall f : \\\\alpha \\\\to \\\\mathbb{R}, \\\\mathrm{Summable}(f) \\\\Rightarrow \\\\forall i : \\\\beta \\\\to \\\\alpha, \\\\mathrm{Injective}(i) \\\\Rightarrow \\\\mathrm{tsum}(f \circ i) \\\\le \\\\mathrm{tsum}(f)$$$
Lean4
theorem tsum_comp_le_tsum_of_inj {β : Type*} {f : α → ℝ} (hf : Summable f) (hn : ∀ a, 0 ≤ f a) {i : β → α}
(hi : Function.Injective i) : tsum (f ∘ i) ≤ tsum f :=
by
lift f to α → ℝ≥0 using hn
rw [NNReal.summable_coe] at hf
simpa only [Function.comp_def, ← NNReal.coe_tsum] using NNReal.tsum_comp_le_tsum_of_inj hf hi
