English
A monoticity-based bound for partial sums with dyadic-type indices holds.
Русский
Условия монотонности дают границу частичных сумм по двойочным индексам.
LaTeX
$$$\\forall f,u,\\; (∀ m,n, ...) \\Rightarrow \\sum_{k< n} (u(k+1)-u(k))\\, f(u(k+1)) ≤ \\sum_{k< n} f(k)$$$
Lean4
/-- for series of nonnegative real numbers. -/
theorem summable_schlomilch_iff_of_nonneg {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ} (h_nonneg : ∀ n, 0 ≤ f n)
(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 : ℝ)) * f (u k)) ↔ Summable f :=
by
lift f to ℕ → ℝ≥0 using h_nonneg
simp only [NNReal.coe_le_coe] at *
have (k : ℕ) : (u (k + 1) - (u k : ℝ)) = ((u (k + 1) : ℝ≥0) - (u k : ℝ≥0) : ℝ≥0) :=
by
have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
simp [NNReal.coe_sub this]
simp_rw [this]
exact_mod_cast NNReal.summable_schlomilch_iff hf h_pos hu_strict hC_nonzero h_succ_diff
