x : ℝ
h : abs x < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
x : ℝ
h : abs x < 1
⊢ HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-log (1 - x))
rw [Summable.hasSum_iff_tendsto_nat]
x : ℝ
h : abs x < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
show Tendsto (fun n : ℕ => ∑ i : ℕ in range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))
x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
show Summable fun n : ℕ => x ^ (n + 1) / (n + 1)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun e => ‖∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
rw [tendsto_iff_norm_tendsto_zero]
x : ℝ
h : abs x < 1
⊢ Tendsto (fun e => abs (∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x))) atTop (𝓝 0)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun e => ‖∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)
simp only [norm_eq_abs, sub_neg_eq_add]
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 0)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun e => abs (∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x))) atTop (𝓝 0)
refine' squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) _
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 (abs x * 0 / (1 - abs x)))
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 0)
suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by
  simpa
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x * abs x ^ t / (1 - abs x)) atTop (𝓝 (abs x * 0 / (1 - abs x)))
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 (abs x * 0 / (1 - abs x)))
simp only [pow_succ]
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ t) atTop (𝓝 0)
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x * abs x ^ t / (1 - abs x)) atTop (𝓝 (abs x * 0 / (1 - abs x)))
refine' (tendsto_const_nhds.mul _).div_const _
no goals
x : ℝ
h : abs x < 1
⊢ Tendsto (fun t => abs x ^ t) atTop (𝓝 0)
exact tendsto_pow_atTop_nhds_0_of_lt_1 (abs_nonneg _) h
no goals
x : ℝ
h : abs x < 1
this : Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 (abs x * 0 / (1 - abs x)))
⊢ Tendsto (fun t => abs x ^ (t + 1) / (1 - abs x)) atTop (𝓝 0)
simpa
x : ℝ
h : abs x < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ abs x ^ i
x : ℝ
h : abs x < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
refine' summable_of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) fun i => _
no goals
x : ℝ
h : abs x < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ abs x ^ i
calc
  ‖x ^ (i + 1) / (i + 1)‖ = |x| ^ (i + 1) / (i + 1) := by
    have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
    rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
  _ ≤ |x| ^ (i + 1) / (0 + 1) := by
    gcongr
    exact i.cast_nonneg
  _ ≤ |x| ^ i := by
    simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)
x : ℝ
h : abs x < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = abs x ^ (i + 1) / (↑i + 1)
x : ℝ
h : abs x < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = abs x ^ (i + 1) / (↑i + 1)
have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
no goals
x : ℝ
h : abs x < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = abs x ^ (i + 1) / (↑i + 1)
rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
case h.bc
x : ℝ
h : abs x < 1
i : ℕ
⊢ 0 ≤ ↑i
x : ℝ
h : abs x < 1
i : ℕ
⊢ abs x ^ (i + 1) / (↑i + 1) ≤ abs x ^ (i + 1) / (0 + 1)
gcongr
no goals
case h.bc
x : ℝ
h : abs x < 1
i : ℕ
⊢ 0 ≤ ↑i
exact i.cast_nonneg
no goals
x : ℝ
h : abs x < 1
i : ℕ
⊢ abs x ^ (i + 1) / (0 + 1) ≤ abs x ^ i
simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)