English
For NNReal sequences with a bounded successor-difference, summability of a Schlomilch-type transformed series is equivalent to summability of f.
Русский
Для NNReal-последовательностей с ограничением разности подряд, суммируемость трансформированной серии по Шломолитчу эквивалентна суммируемости f.
LaTeX
$$$\\forall f,u,\\; (\\text{SuccDiffBounded } C u) \\Rightarrow (\\text{Summable } (k\\mapsto (u(k+1)-u(k))\\, f(u(k)))) \\iff \\text{Summable } f$$$
Lean4
/-- for a series of `NNReal` version. -/
theorem summable_schlomilch_iff {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ≥0} (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m)
(h_pos : ∀ n, 0 < u n) (hu_strict : StrictMono u) (hC_nonzero : C ≠ 0) (h_succ_diff : SuccDiffBounded C u) :
(Summable fun k : ℕ => (u (k + 1) - (u k : ℝ≥0)) * f (u k)) ↔ Summable f :=
by
simp only [← tsum_coe_ne_top_iff_summable, Ne, not_iff_not, ENNReal.coe_mul]
constructor <;> intro h
· replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n => ENNReal.coe_le_coe.2 (f n).2
obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff
simpa [add_eq_top, mul_ne_top, mul_eq_top, hC_nonzero] using eq_top_mono hC h
· replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn => ENNReal.coe_le_coe.2 (hf hm hmn)
have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top
simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict
