-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The Taylor series of the complex logarithm at `1` converges to the logarithm in the
open unit disk. -/
lemma hasSum_taylorSeries_log {z : ℂ} (hz : ‖z‖ < 1) :
    HasSum (fun n : ℕ ↦ (-1) ^ (n + 1) * z ^ n / n) (log (1 + z))

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ (fun x => logTaylor x z - log (1 + z)) =o[atTop] fun x => 1

Tactic:
refine IsLittleO.trans_isBigO ?_ <| isBigO_const_one ℂ (1 : ℝ) atTop

Result:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ (fun x => logTaylor x z - log (1 + z)) =o[atTop] fun _x => 1

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
H : (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n
⊢ (fun n => ‖z‖ ^ n) =o[atTop] fun _x => 1

Tactic:
convert isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz

Result:
case h.e'_8.h
z : ℂ
hz : ‖z‖ < 1
H : (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n
x✝ : ℕ
⊢ 1 = 1 ^ x✝

Proof state:
case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n / 1

Tactic:
gcongr

Result:
case refine_1.inr.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ 1 ≤ ↑n

Proof state:
case h.e'_8.h
z : ℂ
hz : ‖z‖ < 1
H : (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n
x✝ : ℕ
⊢ 1 = 1 ^ x✝

Tactic:
exact (one_pow _).symm

Result:
no goals

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
H : (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n
⊢ (fun x => logTaylor x z - log (1 + z)) =o[atTop] fun _x => 1

Tactic:
refine IsBigO.trans_isLittleO H ?_

Result:
case refine_2
z : ℂ
hz : ‖z‖ < 1
H : (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n
⊢ (fun n => ‖z‖ ^ n) =o[atTop] fun _x => 1

Proof state:
case refine_1
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Result:
case refine_1.inl
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z‖ ^ 0 / ↑0 ≤ ‖z‖ ^ 0

case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Proof state:
case succ.hdb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ 1 ≤ ↑n + 1

Tactic:
linarith

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
this : ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖‖z‖ ^ n‖
⊢ (fun n => logTaylor n z - log (1 + z)) =O[atTop] fun n => ‖z‖ ^ n

Tactic:
exact (isBigOWith_of_le' atTop this).isBigO

Result:
no goals

Proof state:
case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ ∀ (b : ℕ), ‖(-1) ^ (b + 1) * z ^ b / ↑b‖ ≤ ‖z ^ b‖

Tactic:
intro n

Result:
case refine_1
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖(-1) ^ (n + 1) * z ^ n / ↑n‖ ≤ ‖z ^ n‖

Proof state:
case zero
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor 0 z‖ ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ 0

Tactic:
simp [logTaylor_zero]

Result:
no goals

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x => (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)

Tactic:
rw [← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim]

Result:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ (fun x => logTaylor x z - log (1 + z)) =o[atTop] fun x => 1

Proof state:
case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Tactic:
conv => enter [2]; rw [← div_one (‖z‖ ^ n)]

Result:
case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n / 1

Proof state:
case refine_1.inr.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ 1 ≤ ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ Summable fun i => ‖(-1) ^ (i + 1) * z ^ i / ↑i‖

Tactic:
refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_

Result:
case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ ∀ (b : ℕ), ‖(-1) ^ (b + 1) * z ^ b / ↑b‖ ≤ ‖z ^ b‖

Proof state:
case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1) ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ (n + 1)

Tactic:
rw [mul_comm, ← div_one ((max _ _) * _)]

Result:
case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / (↑n + 1) ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ (n + 1) / 1

Proof state:
case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / (↑n + 1) ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ (n + 1) / 1

Tactic:
gcongr

Result:
case succ.hac.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ ≤ ‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹

case succ.hdb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ 1 ≤ ↑n + 1

Proof state:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖logTaylor n z - log (1 + z)‖ ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖‖z‖ ^ n‖

Tactic:
rw [norm_sub_rev, norm_pow, norm_norm]

Result:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor n z‖ ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ n

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x => ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)

Tactic:
conv => enter [1, x]; rw [← div_one (_ - _), ← logTaylor]

Result:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x => (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (log (1 + z))

Tactic:
refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_

Result:
case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ Summable fun i => ‖(-1) ^ (i + 1) * z ^ i / ↑i‖

case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))

Proof state:
case refine_1
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖(-1) ^ (n + 1) * z ^ n / ↑n‖ ≤ ‖z ^ n‖

Tactic:
simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]

Result:
case refine_1
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Proof state:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))

Tactic:
rw [← tendsto_sub_nhds_zero_iff]

Result:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x => ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)

Proof state:
case refine_1.inl
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z‖ ^ 0 / ↑0 ≤ ‖z‖ ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.hac.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ ≤ ‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹

Tactic:
exact le_max_right ..

Result:
no goals

Proof state:
case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ (n + 1)

Tactic:
refine (norm_log_sub_logTaylor_le n hz).trans ?_

Result:
case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1) ≤ (‖log (1 + z)‖ ⊔ (1 - ‖z‖)⁻¹) * ‖z‖ ^ (n + 1)