summable_condensed_iff — Mathlib

English

A condensed sum bound lemma for finite sums with doubling index structure.

Русский

Лемма границы сжатой суммы для конечных сумм с удвоением индексов.

LaTeX

$$$\\forall f,\\ u:\\mathbb{N}\\to\\mathbb{N},\\;\\text{sum condense bound formula}$$$

Lean4

theorem summable_condensed_iff {f : ℕ → ℝ≥0} (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
    (Summable fun k : ℕ => (2 : ℝ≥0) ^ k * f (2 ^ k)) ↔ Summable f :=
  by
  have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
    intro n
    simp [pow_succ, mul_two, two_mul]
  convert
    summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two) two_ne_zero h_succ_diff
  simp [pow_succ, mul_two]

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