English
Under growth and differentiability hypotheses, the Abel-sum partial sums tend to a finite limit; the limit involves the integral of f' times a compensating sum.
Русский
При ростовых и дифференцируемых предпосылках частичные суммы Абеля сходятся к конечному пределу; предел включает интеграл от f' и компенсирующей суммы.
LaTeX
$$$\\text{tendsto }\\left( \\sum_{k ∈ Icc 0 n} f(k) c(k) \\right)_{n\\to\\infty} \\; =\\; l - \\int_{t>0} f'(t) \\sum_{k∈Icc 0 ⌊t⌋} c(k) \\, dt$$$
Lean4
theorem tendsto_sum_mul_atTop_nhds_one_sub_integral (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t)
(hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0)) {l : 𝕜}
(h_lim : Tendsto (fun n : ℕ ↦ f n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)) {g : ℝ → 𝕜}
(hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g) (hg_int : IntegrableAtFilter g atTop) :
Tendsto (fun n : ℕ ↦ ∑ k ∈ Icc 0 n, f k * c k) atTop
(𝓝 (l - ∫ t in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) :=
by
have h_lim' :
Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (0 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
(𝓝 (∫ t in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) :=
by
refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_
refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop
exact
Iff.mp integrableOn_Ici_iff_integrableOn_Ioi <|
(locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop hg_dom hg_int
refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
rw [sum_mul_eq_sub_integral_mul' _ _ (fun t ht ↦ hf_diff _ ht.1)]
exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc
