α : 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
α : 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
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
α : 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
α : 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
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']
α : 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‖
α : 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
apply isLittleO_iff.2 fun ε εpos => _
α : 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‖
α : 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‖
intro ε εpos
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‖
α : 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‖
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)
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‖
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‖
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)
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‖
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‖
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
no goals
α : 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
rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
no goals
α : 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
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
α : 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
α : 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
apply isLittleO_const_left.2
no goals
α : 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
exact Or.inr (h'g.congr fun n => (B n).symm)
no goals
α : 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‖
rw [sum_range_add_sum_Ico _ Nn]
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
α : 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
gcongr
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

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
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
apply sum_le_sum_of_subset_of_nonneg
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
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
rw [range_eq_Ico]
no goals
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
exact Ico_subset_Ico (zero_le _) le_rfl
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
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
intro i _ _
no goals
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
exact mul_nonneg (half_pos εpos).le (hg i)
α : 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
α : 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
rw [← mul_sum]
no goals
α : 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
gcongr
α : 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
α : 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‖
simp only [B]
no goals
α : 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
ring