Kroneckers_Lemma
Provedanalysisproofwikisequences
If b_n increases to infinity and sum(x_n/b_n) converges, then (1/b_n)*sum_{k<=n} x_k -> 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Kroneckers_Lemma (x : ℕ → ℝ) (b : ℕ → ℝ) (hb_pos : ∀ n, 0 < b n) (hb_inc : StrictMono b) (hb_lim : Filter.Tendsto b Filter.atTop Filter.atTop) (hconv : ∃ S, Filter.Tendsto (fun n => ∑ i : Fin n, x i / b i) Filter.atTop (nhds S)) : Filter.Tendsto (fun n => (1 / b n) * ∑ i : Fin n, x i) Filter.atTop (nhds 0) := by sorry
Source