E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun n => (↑n)⁻¹ • ∑ i in range n, u i) atTop (𝓝 l)
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ∑ i in range x, (u i - l)) =ᶠ[atTop] fun n => (↑n)⁻¹ • ∑ i in range n, u i - l

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x => 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ∑ i in range x, (u i - l)) =ᶠ[atTop] fun n => (↑n)⁻¹ • ∑ i in range n, u i - l
filter_upwards [Ici_mem_atTop 1]with n npos
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • n • l = l
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
no goals
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • n • l = l
rw [nsmul_eq_smul_cast ℝ, smul_smul, inv_mul_cancel nposℝ.ne', one_smul]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ↑n = 1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x => 1
filter_upwards [Ici_mem_atTop 1]with n npos
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ↑n = 1
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ↑n = 1
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
no goals
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ↑n = 1
rw [Algebra.id.smul_eq_mul, inv_mul_cancel nposℝ.ne']