[GOAL]
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
  (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne') (ne_of_gt <| exp_pos _) <|
    Eventually.mono (lt_mem_nhds hx) @exp_log
[GOAL]
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (exp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
rwa [exp_log hx] at this 
[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
convert (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
[GOAL]
case h.e'_6
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg
[PROOFSTEP]
ext y
[GOAL]
case h.e'_6.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y
[PROOFSTEP]
exact (log_neg_eq_log y).symm
[GOAL]
case h.e'_7
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1
[PROOFSTEP]
field_simp [hx.ne]
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
exact hasStrictDerivAt_log_of_pos hx
[GOAL]
x✝ x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹
[PROOFSTEP]
rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
[GOAL]
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ n log {0}ᶜ
[PROOFSTEP]
suffices : ContDiffOn ℝ ⊤ log {0}ᶜ
[GOAL]
x : ℝ
n : ℕ∞
this : ContDiffOn ℝ ⊤ log {0}ᶜ
⊢ ContDiffOn ℝ n log {0}ᶜ
case this x : ℝ n : ℕ∞ ⊢ ContDiffOn ℝ ⊤ log {0}ᶜ
[PROOFSTEP]
exact this.of_le le_top
[GOAL]
case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log {0}ᶜ
[PROOFSTEP]
refine' (contDiffOn_top_iff_deriv_of_open isOpen_compl_singleton).2 _
[GOAL]
case this
x : ℝ
n : ℕ∞
⊢ DifferentiableOn ℝ log {0}ᶜ ∧ ContDiffOn ℝ ⊤ (deriv log) {0}ᶜ
[PROOFSTEP]
simp [differentiableOn_log, contDiffOn_inv]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) s x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') s x
[PROOFSTEP]
exact (hasDerivAt_log hx).comp_hasDerivWithinAt x hf
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x
[PROOFSTEP]
exact hf.log hx
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log hx).comp x hf
[GOAL]
t : ℝ
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
have h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t) := by
  simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
    (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
[GOAL]
t : ℝ
⊢ Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
[PROOFSTEP]
simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
  (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
[GOAL]
t : ℝ
⊢ 1 + t * id 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
have h₂ : Tendsto (fun x : ℝ => x⁻¹) atTop (𝓝[≠] 0) :=
  tendsto_inv_atTop_zero'.mono_right (nhdsWithin_mono _ fun x hx => (Set.mem_Ioi.mp hx).ne')
[GOAL]
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[{0}ᶜ] 0)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
simpa only [(· ∘ ·), inv_inv] using h₁.comp h₂
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
let F : ℝ → ℝ := fun x => (∑ i in range n, x ^ (i + 1) / (i + 1)) + log (1 - x)
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
let F' : ℝ → ℝ := fun x ↦
  -x ^ n /
    (1 - x)
      -- Porting note: In `mathlib3`, the proof used `deriv`/`DifferentiableAt`. `simp` failed to
        -- compute `deriv`, so I changed the proof to use `HasDerivAt` instead
        -- First step: compute the derivative of `F`
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := fun y hy ↦
  by
  have : HasDerivAt F ((∑ i in range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
    .add (.sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
      (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
  convert this using 1
  calc
    -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y) :=
      by
      field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
      ring
    _ = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) :=
      by
      congr with i
      rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
        -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ HasDerivAt F (F' y) y
[PROOFSTEP]
have : HasDerivAt F ((∑ i in range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
  .add (.sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
    (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ HasDerivAt F (F' y) y
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_7
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ F' y = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)
[PROOFSTEP]
calc
  -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y) :=
    by
    field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
    ring
  _ = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) :=
    by
    congr with i
    rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
      -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y)
[PROOFSTEP]
field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ -(y ^ n * ((y - 1) * (1 - y))) = ((y ^ n - 1) * (1 - y) + (1 - y)) * (1 - y)
[PROOFSTEP]
ring
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ ∑ i in Finset.range n, y ^ i + -1 / (1 - y) = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)
[PROOFSTEP]
congr with i
[GOAL]
case e_a.e_f.h
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = ↑(i + 1) * y ^ i / (↑i + 1)
[PROOFSTEP]
rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
  -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have B : ∀ y ∈ Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
  calc
    |F' y| = |y| ^ n / |1 - y| := by simp [abs_div]
    _ ≤ |x| ^ n / (1 - |x|) := by
      have : |y| ≤ |x| := abs_le.2 hy
      have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
      gcongr
      exact sub_pos.2 h
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |F' y| = |y| ^ n / |1 - y|
[PROOFSTEP]
simp [abs_div]
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
have : |y| ≤ |x| := abs_le.2 hy
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ 1 - |x| ≤ 1 - y
[PROOFSTEP]
linarith [hy.2]
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this✝ : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
gcongr
[GOAL]
case hd
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this✝ : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
⊢ 0 < 1 - |x|
[PROOFSTEP]
exact sub_pos.2 h
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ :=
  by
  refine
    Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
  · exact Icc_subset_Ioo (neg_lt_neg h) h hy
  · simp
  ·
    simp [le_abs_self x, neg_le.mp (neg_le_abs_self x)]
      -- fourth step: conclude by massaging the inequality of the third step
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
[PROOFSTEP]
refine
  Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
[GOAL]
case refine_1
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ y ∈ Set.Ioo (-1) 1
[PROOFSTEP]
exact Icc_subset_Ioo (neg_lt_neg h) h hy
[GOAL]
case refine_2
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ 0 ∈ Set.Icc (-|x|) |x|
[PROOFSTEP]
simp
[GOAL]
case refine_3
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ x ∈ Set.Icc (-|x|) |x|
[PROOFSTEP]
simp [le_abs_self x, neg_le.mp (neg_le_abs_self x)]
  -- fourth step: conclude by massaging the inequality of the third step
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
simpa [div_mul_eq_mul_div, pow_succ'] using C
[GOAL]
x : ℝ
h : |x| < 1
⊢ HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-log (1 - x))
[PROOFSTEP]
rw [Summable.hasSum_iff_tendsto_nat]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
x : ℝ h : |x| < 1 ⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
show Tendsto (fun n : ℕ => ∑ i : ℕ in range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => ‖∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)
[PROOFSTEP]
simp only [norm_eq_abs, sub_neg_eq_add]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => |∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x)|) atTop (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) _
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
[PROOFSTEP]
suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by simpa
[GOAL]
x : ℝ
h : |x| < 1
this : Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
[PROOFSTEP]
simpa
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
[PROOFSTEP]
simp only [pow_succ]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
[PROOFSTEP]
refine' (tendsto_const_nhds.mul _).div_const _
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ t) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_pow_atTop_nhds_0_of_lt_1 (abs_nonneg _) h
[GOAL]
x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
show Summable fun n : ℕ => x ^ (n + 1) / (n + 1)
[GOAL]
x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
refine' summable_of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) fun i => _
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ |x| ^ i
[PROOFSTEP]
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)
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)
[PROOFSTEP]
have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)
[PROOFSTEP]
rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (↑i + 1) ≤ |x| ^ (i + 1) / (0 + 1)
[PROOFSTEP]
gcongr
[GOAL]
case h.bc
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ ↑i
[PROOFSTEP]
exact i.cast_nonneg
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (0 + 1) ≤ |x| ^ i
[PROOFSTEP]
simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)
[GOAL]
x : ℝ
h : |x| < 1
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
set term := fun n : ℕ => -1 * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + x ^ (n + 1) / (n + 1)
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
have h_term_eq_goal : term ∘ (· * ·) 2 = fun k : ℕ => 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1) :=
  by
  ext n
  dsimp only [(· ∘ ·)]
  rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
  push_cast
  ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
[PROOFSTEP]
ext n
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ (term ∘ (fun x x_1 => x * x_1) 2) n = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
dsimp only [(· ∘ ·)]
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * ((-x) ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) =
    2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
push_cast
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (2 * ↑n + 1)) + x ^ (2 * n + 1) / (2 * ↑n + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))
[PROOFSTEP]
have h₁ := (hasSum_pow_div_log_of_abs_lt_1 (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ HasSum term (log (1 + x) - log (1 - x))
[PROOFSTEP]
convert h₁.add (hasSum_pow_div_log_of_abs_lt_1 h) using 1
[GOAL]
case h.e'_6
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)
[PROOFSTEP]
ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ (x : ℕ), ¬x ∈ Set.range ((fun x x_1 => x * x_1) 2) → term x = 0
[PROOFSTEP]
intro m hm
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : ¬m ∈ Set.range ((fun x x_1 => x * x_1) 2)
⊢ term m = 0
[PROOFSTEP]
rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm 
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0
[PROOFSTEP]
dsimp
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ -1 * ((-x) ^ (m + 1) / (↑m + 1)) + x ^ (m + 1) / (↑m + 1) = 0
[PROOFSTEP]
rw [Even.neg_pow hm, neg_one_mul, neg_add_self]
[GOAL]
a : ℝ
h : 0 < a
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
[PROOFSTEP]
have h₁ : |1 / (2 * a + 1)| < 1 := by
  rw [abs_of_pos, div_lt_one]
  · linarith
  · linarith
  · exact div_pos one_pos (by linarith)
[GOAL]
a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1
[PROOFSTEP]
rw [abs_of_pos, div_lt_one]
[GOAL]
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)
[PROOFSTEP]
exact div_pos one_pos (by linarith)
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
[PROOFSTEP]
convert hasSum_log_sub_log_of_abs_lt_1 h₁ using 1
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
[GOAL]
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ 2 * a + 1 ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
have h₃ := h.ne'
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
rw [← log_div]
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
[PROOFSTEP]
congr
[GOAL]
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6.hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
[PROOFSTEP]
field_simp
