le_sum_schlomilch — Mathlib

English

A Schlomilch-type bound relating sums over an interval Ico(u0+1, u n+1) to a weighted sum over f(u k).

Русский

Граница типа Шломолитч между суммой по Ico(u0+1, u n+1) и взвешенной суммой по f(u k).

LaTeX

$$$\\forall hf,\\; \\sum_{k\\in \\range (u n)} f(k) ≤ \\sum_{k\\in \\Ico(u0+1,u n+1)} f(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 ∈ range (u n), f k) ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) :=
  by
  convert add_le_add_left (le_sum_schlomilch' hf h_pos hu n) (∑ k ∈ range (u 0), f k)
  rw [← sum_range_add_sum_Ico _ (hu n.zero_le)]

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