English
The ENNReal sum of a shifted sequence is bounded by a sum of the tail of f plus a constant times a base sum.
Русский
Сумма ENNReal после смещения ограничена суммой хвоста и константой, умноженной на базовую сумму.
LaTeX
$$$\\sum'_{k} (u(k+1)-u(k)) \\cdot f(u(k)) \\le (u(1)-u(0))f(u(0)) + C \\sum'_{k} f(k)$$$
Lean4
theorem le_tsum_schlomilch (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n) (hu : StrictMono u) :
∑' k, f k ≤ ∑ k ∈ range (u 0), f k + ∑' k : ℕ, (u (k + 1) - u k) * f (u k) :=
by
rw [ENNReal.tsum_eq_iSup_nat' hu.tendsto_atTop]
refine iSup_le fun n => (Finset.le_sum_schlomilch hf h_pos hu.monotone n).trans (add_le_add_left ?_ _)
have (k : ℕ) : (u (k + 1) - u k : ℝ≥0∞) = (u (k + 1) - (u k : ℕ) : ℕ) := by simp
simp only [nsmul_eq_mul, this]
apply ENNReal.sum_le_tsum
