α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ a, ∀ (b : ℕ), b ≥ a → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f
rw [eventually_atTop] at h
case intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ a, ∀ (b : ℕ), b ≥ a → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
rcases h with ⟨N₀, hN₀⟩
case intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
case intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
rw [frequently_atTop] at hf
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable f
case intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable fun n => f (n + N)
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable f
rw [← @summable_nat_add_iff α _ _ _ _ N]
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable fun n => f (n + N)
refine' mt Summable.tendsto_atTop_zero
  fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') _
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0

case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) n ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (n + 1)
case intro.intro.intro
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop
convert tendsto_atTop_of_geom_le _ hr _
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
refine' lt_of_le_of_ne (norm_nonneg _) _
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
⊢ False
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
intro h''
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
⊢ False
specialize hN₀ N hNN₀
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False
simp only [comp_apply, zero_add] at h''
no goals
case intro.intro.intro.convert_2
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False
exact hN h''.symm
case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) i ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (i + 1)
case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) n ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (n + 1)
intro i
case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ‖f (i + N)‖ ≤ ‖f (i + 1 + N)‖
case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) i ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (i + 1)
dsimp only [comp_apply]
case h.e'_4.h.e'_3.h.e'_1
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ i + 1 + N = i + N + 1
case intro.intro.intro.convert_3
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ‖f (i + N)‖ ≤ ‖f (i + 1 + N)‖
convert hN₀ (i + N) (hNN₀.trans (N.le_add_left i)) using 3
no goals
case h.e'_4.h.e'_3.h.e'_1
α✝ : Type ?u.1330271
β : Type ?u.1330274
ι : Type ?u.1330277
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ i + 1 + N = i + N + 1
ac_rfl