English
Various simplifications (simp) about sum_range lemma under isLittleO; used as supporting facts.
Русский
Различные упрощения (simp) для леммы sum_range под isLittleO, служат опорными фактами.
LaTeX
$$$ (\text{isLittleO sum_range lemma}) $$$
Lean4
/-- The Cesaro average of a converging sequence converges to the same limit. -/
theorem cesaro_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : ℕ → E} {l : E}
(h : Tendsto u atTop (𝓝 l)) : Tendsto (fun n : ℕ => (n⁻¹ : ℝ) • ∑ i ∈ range n, u i) atTop (𝓝 l) :=
by
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
· filter_upwards [Ici_mem_atTop 1] with n npos
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]
· filter_upwards [Ici_mem_atTop 1] with n npos
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
rw [Algebra.id.smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']
