α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
rw [tsum_eq_zero_add (NormedRing.summable_geometric_of_norm_lt_1 x h)]
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
simp only [_root_.pow_zero]
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
refine' le_trans (norm_add_le _ _) _
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by
  refine' tsum_of_norm_bounded _ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
  convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_1 (norm_nonneg x) h)
  simp
no goals
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
linarith
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun b => ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
refine' tsum_of_norm_bounded _ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
case h.e'_6.h.e'_6
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ 1 = ∑ i in Finset.range 1, ‖x‖ ^ i
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun b => ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_1 (norm_nonneg x) h)
no goals
case h.e'_6.h.e'_6
α : Type ?u.1234446
β : Type ?u.1234449
ι : Type ?u.1234452
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ 1 = ∑ i in Finset.range 1, ‖x‖ ^ i
simp