[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ f =o[𝓝[{a}ᶜ] a] fun x => (x - a)⁻¹
[PROOFSTEP]
refine' (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[{a}ᶜ] a) atTop
[PROOFSTEP]
simp only [(· ∘ ·), norm_inv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[{a}ᶜ] a) atTop
[PROOFSTEP]
exact (tendsto_norm_sub_self_punctured_nhds a).inv_tendsto_zero
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atTop] fun x => x ^ (↑p - ↑q)
[PROOFSTEP]
apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), 0 < x → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : 0 < x
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
simp [zpow_sub₀ hx.ne']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atBot] fun x => x ^ (↑p - ↑q)
[PROOFSTEP]
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), x < 0 → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
simp [zpow_sub₀ hx.ne]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℤ
hn : 0 < n
⊢ Tendsto (fun x => x ^ n) atTop atTop
[PROOFSTEP]
lift n to ℕ using hn.le
[GOAL]
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop
[PROOFSTEP]
simp only [zpow_ofNat]
[GOAL]
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ n) atTop atTop
[PROOFSTEP]
exact tendsto_pow_atTop (Nat.cast_pos.mp hn).ne'
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop atTop
[PROOFSTEP]
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop (𝓝 0)
[PROOFSTEP]
apply tendsto_zpow_atTop_zero
[GOAL]
case hn
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ↑p - ↑q < 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ (fun x => x ^ p) =o[atTop] fun x => x ^ q
[PROOFSTEP]
refine' (isLittleO_iff_tendsto' _).mpr (tendsto_pow_div_pow_atTop_zero hpq)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0
[PROOFSTEP]
exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim
[GOAL]
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
rcases huv.exists_pos with ⟨c, hc, hcuv⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
rw [IsBigOWith] at hcuv 
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
convert Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c
[PROOFSTEP]
rw [mul_div_cancel_left _ hc.ne.symm]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
have B : ∀ n, ‖∑ i in range n, g i‖ = ∑ i in range n, g i := fun n => by rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
⊢ ‖∑ i in range n, g i‖ = ∑ i in range n, g i
[PROOFSTEP]
rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
apply isLittleO_iff.2 fun ε εpos => _
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
intro ε εpos
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
  simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
[PROOFSTEP]
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
[GOAL]
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
have : (fun _ : ℕ => ∑ i in range N, f i) =o[atTop] fun n : ℕ => ∑ i in range n, g i :=
  by
  apply isLittleO_const_left.2
  exact Or.inr (h'g.congr fun n => (B n).symm)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
apply isLittleO_const_left.2
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∑ i in range N, f i = 0 ∨ Tendsto (norm ∘ fun n => ∑ i in range n, g i) atTop atTop
[PROOFSTEP]
exact Or.inr (h'g.congr fun n => (B n).symm)
[GOAL]
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
[GOAL]
case h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range n, f i‖ ≤ ε * ‖∑ i in range n, g i‖
[PROOFSTEP]
calc
  ‖∑ i in range n, f i‖ = ‖(∑ i in range N, f i) + ∑ i in Ico N n, f i‖ := by rw [sum_range_add_sum_Ico _ Nn]
  _ ≤ ‖∑ i in range N, f i‖ + ‖∑ i in Ico N n, f i‖ := (norm_add_le _ _)
  _ ≤ ‖∑ i in range N, f i‖ + ∑ i in Ico N n, ε / 2 * g i :=
    (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
  _ ≤ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i :=
    by
    gcongr
    apply sum_le_sum_of_subset_of_nonneg
    · rw [range_eq_Ico]
      exact Ico_subset_Ico (zero_le _) le_rfl
    · intro i _ _
      exact mul_nonneg (half_pos εpos).le (hg i)
  _ ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i := by rw [← mul_sum]; gcongr
  _ = ε * ‖∑ i in range n, g i‖ := by
    simp only [B]
    ring
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range n, f i‖ = ‖∑ i in range N, f i + ∑ i in Ico N n, f i‖
[PROOFSTEP]
rw [sum_range_add_sum_Ico _ Nn]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ∑ i in Ico N n, ε / 2 * g i ≤ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i
[PROOFSTEP]
gcongr
[GOAL]
case bc
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ∑ i in Ico N n, ε / 2 * g i ≤ ∑ i in range n, ε / 2 * g i
[PROOFSTEP]
apply sum_le_sum_of_subset_of_nonneg
[GOAL]
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ range n
[PROOFSTEP]
rw [range_eq_Ico]
[GOAL]
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n
[PROOFSTEP]
exact Ico_subset_Ico (zero_le _) le_rfl
[GOAL]
case bc.hf
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ∀ (i : ℕ), i ∈ range n → ¬i ∈ Ico N n → 0 ≤ ε / 2 * g i
[PROOFSTEP]
intro i _ _
[GOAL]
case bc.hf
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
i : ℕ
a✝¹ : i ∈ range n
a✝ : ¬i ∈ Ico N n
⊢ 0 ≤ ε / 2 * g i
[PROOFSTEP]
exact mul_nonneg (half_pos εpos).le (hg i)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i
[PROOFSTEP]
rw [← mul_sum]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ε / 2 * ∑ x in range n, g x ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i = ε * ‖∑ i in range n, g i‖
[PROOFSTEP]
simp only [B]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ∑ i in range n, g i + ε / 2 * ∑ i in range n, g i = ε * ∑ i in range n, g i
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i in range n, 1) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, 1
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
simp only [sum_const, card_range, Nat.smul_one_eq_coe] at this 
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
exact this tendsto_nat_cast_atTop_atTop
[GOAL]
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)
[PROOFSTEP]
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
[GOAL]
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
[PROOFSTEP]
have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
[GOAL]
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
[PROOFSTEP]
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
[GOAL]
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
[PROOFSTEP]
filter_upwards [Ici_mem_atTop 1] with n npos
[GOAL]
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
[PROOFSTEP]
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
[GOAL]
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
[PROOFSTEP]
simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
[GOAL]
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
[PROOFSTEP]
rw [nsmul_eq_smul_cast ℝ, smul_smul, inv_mul_cancel nposℝ.ne', one_smul]
[GOAL]
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
[PROOFSTEP]
filter_upwards [Ici_mem_atTop 1] with n npos
[GOAL]
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
[PROOFSTEP]
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
[GOAL]
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
[PROOFSTEP]
rw [Algebra.id.smul_eq_mul, inv_mul_cancel nposℝ.ne']
