le_sum_condensed' — Mathlib

English

A variant of Schlomilch-type bound on sums with shifted indices, under similar monotone and positivity assumptions.

Русский

Вариант границы Шлохломича для сумм со сдвинутыми индексами при аналогичных условиях монотонности и неотрицательности.

LaTeX

$$$\\forall hf,\\ n:\\; \\sum_{k\\in Ico(u0+1,u n+1)} f(k) \\ge ?$$$

Lean4

theorem le_sum_condensed' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
    (∑ k ∈ Ico 1 (2 ^ n), f k) ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k) :=
  by
  convert le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n) (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
  simp [pow_succ, mul_two]

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