English
If the derivative and the sum are big-O of certain functions, then the partial sums of f(k)c(k) converge to the predicted constant minus an integral term.
Русский
Если производная и сумма ведут себя как O-относительно некоторой функции, то частичные суммы сходятся к предсказанному константному члену минус интегральный член.
LaTeX
$$$\\text{tendsto }(\\sum_{k ≤ n} f(k)c(k))_{n} = l - \\int_{a}^{b} f'(t) \\sum_{k≤⌊t⌋} c(k) dt$$$
Lean4
theorem tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (hc : c 0 = 0) (hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t)
(hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1)) {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 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) :=
by
have h :
(fun n : ℕ ↦ ∫ (x : ℝ) in (1 : ℝ)..n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop]
(fun n : ℕ ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) :=
by
filter_upwards [eventually_ge_atTop 1] with _ h
rw [← integral_of_le (Nat.one_le_cast.mpr h)]
have h_lim' :
Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (1 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
(𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) :=
by
refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
exact
Iff.mp integrableOn_Ici_iff_integrableOn_Ioi <|
(locallyIntegrableOn_mul_sum_Icc c zero_le_one 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₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]
exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc
