English
For a monotone, antitone-type inequality on f and a monotone u, the partial sums of f up to u(n) are bounded by a weighted sum of the tail values of f at u(k).
Русский
Пусть f удовлетворяет обратному неравенству и функция u монотонна; тогда частичные суммы до u(n) ограничиваются суммой весов, умноженных на соответствующие значения f(u(k)).
LaTeX
$$$\\forall hf,\\ h_pos,\\ hu,\\ n:\\; \\sum_{k\\in Ico(u0,u n)} f(k) \\le \\sum_{k\\in\\mathrm{range}\\ n} (u(k+1)-u(k))\\, f(u(k))$$$
Lean4
theorem le_sum_schlomilch' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n) (hu : Monotone u) (n : ℕ) :
(∑ k ∈ Ico (u 0) (u n), f k) ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) := by
induction n with
| zero => simp
| succ n
ihn =>
suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n)
by
rw [sum_range_succ, ← sum_Ico_consecutive]
· exact add_le_add ihn this
exacts [hu n.zero_le, hu n.le_succ]
have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk => hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
convert sum_le_sum this
simp
