α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
have xi_ne_one : ξ ≠ 1 := by
  contrapose! h
  simp [h]
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
  ((tendsto_pow_atTop_nhds_0_of_norm_lt_1 h).sub tendsto_const_nhds).mul tendsto_const_nhds
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i in Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i => ‖ξ ^ i‖
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
rw [hasSum_iff_tendsto_nat_of_summable_norm]
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1
contrapose! h
no goals
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖
simp [h]
no goals
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i in Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)
simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A
no goals
α : Type ?u.133909
β : Type ?u.133912
ι : Type ?u.133915
K : Type u_1
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i => ‖ξ ^ i‖
simp [norm_pow, summable_geometric_of_lt_1 (norm_nonneg _) h]