le_tsum_condensed — Mathlib

English

A bound for the total sum in terms of a base sum and a tail sum with Schlomilch-type weights.

Русский

Граница на полную сумму через базовую и хвостовую суммы с весами Шломолитч-подобными.

LaTeX

$$$\\sum'_{k} f(k) ≤ (u(0)) + \\sum'_{k} (u(k+1)-u(k)) f(u(k))$$$

Lean4

theorem le_tsum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) : ∑' k, f k ≤ f 0 + ∑' k : ℕ, 2 ^ k * f (2 ^ k) :=
  by
  rw [ENNReal.tsum_eq_iSup_nat' (Nat.tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]
  refine iSup_le fun n => (Finset.le_sum_condensed hf n).trans (add_le_add_left ?_ _)
  simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]
  apply ENNReal.sum_le_tsum

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