tsum_condensed_le — Mathlib

English

A condensed-name bound for ENNReal sums comparing a double-indexed sum to a single-index sum.

Русский

Упрощённая граница ENNReal сумм, сравнивающая двойную индексацию и одну сумму.

LaTeX

$$$\\sum'_{k} 2^k f(2^k) ≤ f(1) + 2 \\sum'_{k} f(k)$$$

Lean4

theorem tsum_condensed_le (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) :
    (∑' k : ℕ, 2 ^ k * f (2 ^ k)) ≤ f 1 + 2 * ∑' k, f k :=
  by
  rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]
  refine
    iSup_le fun n =>
      le_trans ?_ (add_le_add_left (nsmul_le_nsmul_right (ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)) _) _)
  simpa using Finset.sum_condensed_le hf n

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