-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.IsLittleO.sum_range {α : Type*} [NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ}
    (h : f =o[atTop] g) (hg : 0 ≤ g) (h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop) :
    (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Proof state:
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖

Tactic:
have : (fun _ : ℕ => ∑ i ∈ range N, f i) =o[atTop] fun n : ℕ => ∑ i ∈ range n, g i := by
  apply isLittleO_const_left.2
  exact Or.inr (h'g.congr fun n => (B n).symm)

Result:
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b

Tactic:
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)

Result:
no goals

Proof state:
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n

Tactic:
exact Ico_subset_Ico (zero_le _) le_rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Tactic:
apply isLittleO_iff.2 fun ε εpos => _

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Tactic:
have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by
  rwa [Real.norm_eq_abs, abs_sum_of_nonneg']

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Proof state:
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖

Tactic:
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn

Result:
case h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ range n, f i‖ ≤ ε * ‖∑ i ∈ range n, g i‖

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ range n, f i‖ = ‖∑ i ∈ range N, f i + ∑ i ∈ Ico N n, f i‖

Tactic:
rw [sum_range_add_sum_Ico _ Nn]

Result:
no goals

Proof state:
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ range n

Tactic:
rw [range_eq_Ico]

Result:
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Tactic:
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
⊢ ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i

Tactic:
rwa [Real.norm_eq_abs, abs_sum_of_nonneg']

Result:
no goals