English
A global bound for ENNReal sums with Schlomilch-type decomposition.
Русский
Глобальная граница для ENNReal сумм с разложением типа Шломолитч.
LaTeX
$$$\\text{tsum } f(k) ≤ (\\text{range }(u0)) + \\text{tsum}(f(k))$$$
Lean4
theorem tsum_schlomilch_le {C : ℕ} (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
(h_nonneg : ∀ n, 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) :
∑' k : ℕ, (u (k + 1) - u k) * f (u k) ≤ (u 1 - u 0) * f (u 0) + C * ∑' k, f k :=
by
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id)]
refine
iSup_le fun n =>
le_trans ?_
(add_le_add_left (mul_le_mul_of_nonneg_left (ENNReal.sum_le_tsum <| Finset.Ico (u 0 + 1) (u n + 1)) ?_) _)
· simpa using Finset.sum_schlomilch_le hf h_pos h_nonneg hu h_succ_diff n
· exact zero_le _
