English
A Schlomilch-type inequality relating sums over ranges with shifted indices.
Русский
Неравенство типа Шломолитч для сумм по диапазонам с сдвинутыми индексами.
LaTeX
$$$\\forall f,u,\\; \\text{(Schlomilch-type inequality with ranges)}$$$
Lean4
/-- Cauchy condensation test for antitone series of nonnegative real numbers. -/
theorem summable_condensed_iff_of_nonneg {f : ℕ → ℝ} (h_nonneg : ∀ n, 0 ≤ f n)
(h_mono : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) : (Summable fun k : ℕ => (2 : ℝ) ^ 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_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two) (pow_right_strictMono₀ one_lt_two)
two_ne_zero h_succ_diff
simp [pow_succ, mul_two]
