case pos
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : ¬0 ≤ r
⊢ Summable f
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f
by_cases hr₀ : 0 ≤ r
case pos
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ (b : ℕ), b ≥ a → ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f
case pos
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f
rw [eventually_atTop] at h
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f
case pos
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ (b : ℕ), b ≥ a → ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f
rcases h with ⟨N, hN⟩
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n => f (n + N)
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f
rw [← @summable_nat_add_iff α _ _ _ _ N]
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ (fun n => ‖f N‖ * r ^ n) n
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n => f (n + N)
refine' summable_of_norm_bounded (fun n ↦ ‖f N‖ * r ^ n)
  (Summable.mul_left _ <| summable_geometric_of_lt_1 hr₀ hr₁) fun n ↦ _
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ (fun n => ‖f N‖ * r ^ n) n
simp only
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n
conv_rhs => rw [mul_comm, ← zero_add N]
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ (fun n => ‖f (n + N)‖) (i + 1) ≤ r * (fun n => ‖f (n + N)‖) i
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
refine' le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ _
case h.e'_3.h.e'_3.h.e'_1
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1
case pos.intro
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ (fun n => ‖f (n + N)‖) (i + 1) ≤ r * (fun n => ‖f (n + N)‖) i
convert hN (i + N) (N.le_add_left i) using 3
no goals
case h.e'_3.h.e'_3.h.e'_1
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1
ac_rfl
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : ¬0 ≤ r
⊢ Summable f
push_neg at hr₀
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖f i‖ ≤ OfNat.ofNat 0 i
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
refine' summable_of_norm_bounded_eventually 0 summable_zero _
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ OfNat.ofNat 0 i
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖f i‖ ≤ OfNat.ofNat 0 i
rw [Nat.cofinite_eq_atTop]
case h
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
⊢ ‖f a✝‖ ≤ OfNat.ofNat 0 a✝
case neg
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ OfNat.ofNat 0 i
filter_upwards [h]with _ hn
case h
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h✝ : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
h : OfNat.ofNat 0 a✝ < ‖f a✝‖
⊢ False
case h
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
⊢ ‖f a✝‖ ≤ OfNat.ofNat 0 a✝
by_contra' h
no goals
case h
α✝ : Type ?u.1269724
β : Type ?u.1269727
ι : Type ?u.1269730
α : Type u_1
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h✝ : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
h : OfNat.ofNat 0 a✝ < ‖f a✝‖
⊢ False
exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)