awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₆ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
linarith₈ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₉ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₀ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
linarith₁₅ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₆ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
linarith₁₈ :
  3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ →
    1 * HPow.hPow (β := ℕ) (1 * ‖z‖) 2 * (1 * (1 - ‖z‖)⁻¹) - 1 * ‖z‖ +
        (HMul.hMul (α := ℝ) 1 3 * (1 * ‖z‖) - (1 * HPow.hPow (β := ℕ) (1 * ‖z‖) 2 * (1 * (1 - ‖z‖)⁻¹) + 2 * ‖z‖)) =
      0
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
rw : ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [sub_eq_add_neg,
    log_inv _ <| slitPlane_arg_ne_pi <| mem_slitPlane_of_norm_lt_one <| (norm_neg z).symm ▸ hz,
    ← sub_neg_eq_add, ← neg_sub', norm_neg]

Premises used: Complex.log_inv, sub_eq_add_neg, Complex.mem_slitPlane_of_norm_lt_one, neg_sub', norm_neg, Complex.slitPlane_arg_ne_pi, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖-z‖ ^ (n + 1) * (1 - ‖-z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz

Premises used: Complex.norm_log_sub_logTaylor_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
h : ‖z‖ = ‖-z‖
h₁ : 1 - ‖z‖ = 1 - ‖-z‖
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
convert! norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz using 4

Premises used: Complex.norm_log_sub_logTaylor_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
h h₁ : ‖z‖ = ‖z‖
⊢ ‖z‖ = ‖-z‖

Tactic:
rw [norm_neg]

Premises used: norm_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
h h₁ : 1 - ‖z‖ = 1 - ‖z‖
⊢ 1 - ‖z‖ = 1 - ‖-z‖

Tactic:
rw [norm_neg]

Premises used: norm_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ + logTaylor (HAdd.hAdd (α := ℕ) 1 1) (-z)‖ ≤
    ‖z‖ ^ HAdd.hAdd (α := ℕ) 1 1 * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1

Tactic:
norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz

Premises used: Complex.norm_log_one_sub_inv_add_logTaylor_neg_le, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (HAdd.hAdd (α := ℕ) 1 1) (-z)
h₁ : 2 = HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
⊢ ‖log (1 - z)⁻¹ - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2

Tactic:
convert! norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2

Premises used: Complex.norm_log_one_sub_inv_add_logTaylor_neg_le, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (HAdd.hAdd (α := ℕ) 1 1) (-z)

Tactic:
simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Complex.logTaylor_zero, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) (log (1 + z))

Tactic:
(hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_

Premises used: Iff.mpr, hasSum_iff_tendsto_nat_of_summable_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_1 : Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖
refine_2 :
  Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)) atTop
    (nhds (log (1 + z)))
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) (log (1 + z))

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

Premises used: Iff.mpr, hasSum_iff_tendsto_nat_of_summable_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖

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

Premises used: HMul.hMul, HDiv.hDiv, Summable.of_nonneg_of_le, Nat.cast, HPow.hPow, HAdd.hAdd, Summable.norm, summable_geometric_of_norm_lt_one, OfNat.ofNat, norm_nonneg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_1 : ∀ (b : ℕ), ‖HPow.hPow (α := ℂ) (-1) (b + 1) * z ^ b / (↑b : ℂ)‖ ≤ ‖z ^ b‖
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖

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

Premises used: Summable.of_nonneg_of_le, Summable.norm, summable_geometric_of_norm_lt_one, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
refine_1 : ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
⊢ ‖HPow.hPow (α := ℂ) (-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]

Premises used: one_pow, norm_pow, Complex.norm_natCast, NormOneClass.norm_one, norm_mul, norm_div, norm_neg, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
refine_1 : HPow.hPow (β := ℕ) ‖z‖ 0 / (↑0 : ℝ) ≤ HPow.hPow (β := ℕ) ‖z‖ 0
refine_1₁ : ∀ (hn : n > 0), ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HPow.hPow (β := ℕ) ‖z‖ 0 / (↑0 : ℝ) ≤ HPow.hPow (β := ℕ) ‖z‖ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
enter : ‖z‖ ^ n
| ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n

Tactic:
enter [2]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
rw : ‖z‖ ^ n / 1
| ‖z‖ ^ n

Tactic:
rw [← div_one (‖z‖ ^ n)]

Premises used: Norm.norm, HPow.hPow, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
enter : ‖z‖ ^ n / 1
| ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n

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

Premises used: Norm.norm, HPow.hPow, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
refine_1 : ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n / 1
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n

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

Premises used: Norm.norm, HPow.hPow, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
refine_1 : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n / 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
refine_1 refine_1₁ refine_1₂ refine_1₃ : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_2 :
  Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)) atTop
    (nhds (log (1 + z)))

Tactic:
rw [← tendsto_sub_nhds_zero_iff]

Premises used: tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : ∀ (x : ℕ), ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)
| Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)

Tactic:
enter [1, x]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
x : ℕ
h : (logTaylor x z - log (1 + z)) / 1
| ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)

Tactic:
rw [← div_one (_ - _), ← logTaylor]

Premises used: HSub.hSub, div_one, Complex.logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : ∀ (x : ℕ), (logTaylor x z - log (1 + z)) / 1
| Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)

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

Premises used: HSub.hSub, div_one, Complex.logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_2 : Tendsto (β := ℂ) (fun (x : ℕ) ↦ (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)
⊢ Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)

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

Premises used: HSub.hSub, div_one, Complex.logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_2 : IsLittleO (E := ℂ) (F := ℂ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (x : ℕ) ↦ 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]

Premises used: False.elim, Asymptotics.isLittleO_iff_tendsto, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ IsLittleO (E := ℂ) (F := ℂ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (x : ℕ) ↦ 1

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

Premises used: Asymptotics.isBigO_const_one, Filter.atTop, Complex, OfNat.ofNat, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_2 : IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1
⊢ IsLittleO (E := ℂ) (F := ℂ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (x : ℕ) ↦ 1

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

Premises used: Asymptotics.isBigO_const_one, Filter.atTop, Complex, OfNat.ofNat, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
rw : ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ n
⊢ ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖

Tactic:
rw [norm_sub_rev, norm_pow, norm_norm]

Premises used: norm_pow, norm_norm, norm_sub_rev
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor 0 z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * HPow.hPow (β := ℕ) ‖z‖ 0

Tactic:
simp [logTaylor_zero]

Premises used: Complex.logTaylor_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)

Tactic:
(norm_log_sub_logTaylor_le n hz).trans ?_

Premises used: Complex.norm_log_sub_logTaylor_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
succ : ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)

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

Premises used: Complex.norm_log_sub_logTaylor_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
succ : (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)

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

Premises used: HMul.hMul, Max.max, mul_comm, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
succ : (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹
succ₁ : 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹

Tactic:
le_max_right ..

Premises used: le_max_right
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹

Tactic:
exact le_max_right ..

Premises used: le_max_right
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < 1 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 1) = 0
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
zero : ‖log (1 + z) - logTaylor 0 z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * HPow.hPow (β := ℕ) ‖z‖ 0
succ : ∀ (n : ℕ), ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
⊢ ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ n

Tactic:
cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith

Premises used: le_max_right, HMul.hMul, Complex.norm_log_sub_logTaylor_le, Max.max, Complex.logTaylor_zero, mul_comm, LE.le.trans, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖

Tactic:
have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
this : ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n

Tactic:
(isBigOWith_of_le' atTop this).isBigO

Premises used: Asymptotics.isBigOWith_of_le', Filter.atTop, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
this : ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n

Tactic:
exact (isBigOWith_of_le' atTop this).isBigO

Premises used: Asymptotics.isBigOWith_of_le', Filter.atTop, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n

Tactic:
have H : (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] (fun n : ℕ ↦ ‖z‖ ^ n) := by
      have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
      exact (isBigOWith_of_le' atTop this).isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1

Tactic:
IsBigO.trans_isLittleO H ?_

Premises used: Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
refine_2 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖z‖ ^ n) fun (_x : ℕ) ↦ 1
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1

Tactic:
refine IsBigO.trans_isLittleO H ?_

Premises used: Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖z‖ ^ n) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) 1 n

Tactic:
isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz

Premises used: isLittleO_pow_pow_of_lt_left, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
h : ∀ (x : ℕ), 1 = HPow.hPow (α := ℝ) 1 x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖z‖ ^ n) fun (_x : ℕ) ↦ 1

Tactic:
convert! isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz

Premises used: isLittleO_pow_pow_of_lt_left, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
x : ℕ
⊢ 1 = HPow.hPow (α := ℝ) 1 x

Tactic:
(one_pow _).symm

Premises used: one_pow, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
x : ℕ
⊢ 1 = HPow.hPow (α := ℝ) 1 x

Tactic:
exact (one_pow _).symm

Premises used: one_pow, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : ∀ (n : ℕ), z ^ n / (↑n : ℂ)
| HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))

Tactic:
enter [1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
h : - -(z ^ n / (↑n : ℂ))
| z ^ n / (↑n : ℂ)

Tactic:
rw [← neg_neg (z ^ n / n)]

Premises used: neg_neg, HDiv.hDiv, Nat.cast, HPow.hPow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : ∀ (n : ℕ), - -(z ^ n / (↑n : ℂ))
| HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))

Tactic:
enter [1, n]; rw [← neg_neg (z ^ n / n)]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
conv : HasSum (fun (n : ℕ) ↦ - -(z ^ n / (↑n : ℂ))) (-log (1 - z))
⊢ HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))

Tactic:
conv => enter [1, n]; rw [← neg_neg (z ^ n / n)]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ - -(z ^ n / (↑n : ℂ))) (-log (1 - z))

Tactic:
HasSum.neg ?_

Premises used: HasSum.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
refine : HasSum (fun (n : ℕ) ↦ -(z ^ n / (↑n : ℂ))) (log (1 - z))
⊢ HasSum (fun (n : ℕ) ↦ - -(z ^ n / (↑n : ℂ))) (-log (1 - z))

Tactic:
refine HasSum.neg ?_

Premises used: HasSum.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)) (log (1 + -z))

Tactic:
hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz)

Premises used: Eq.rec, norm_neg, Complex.hasSum_taylorSeries_log, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : ∀ (n : ℕ), -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
⊢ HasSum (fun (n : ℕ) ↦ -(z ^ n / (↑n : ℂ))) (log (1 - z))

Tactic:
convert! hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz) using 2 with n

Premises used: Eq.rec, norm_neg, Complex.hasSum_taylorSeries_log, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
h :
  -(HPow.hPow (β := ℕ) z 0 / (↑0 : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (HAdd.hAdd (α := ℕ) 0 1) * HPow.hPow (β := ℕ) (-z) 0 / (↑0 : ℂ)
h₁ : ∀ (hn : n > 0), -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
⊢ -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ -(HPow.hPow (β := ℕ) z 0 / (↑0 : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (HAdd.hAdd (α := ℕ) 0 1) * HPow.hPow (β := ℕ) (-z) 0 / (↑0 : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)

Tactic:
simp [field, pow_add, ← mul_pow]

Premises used: pow_add, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) atTop (𝓝 t)

Tactic:
apply hg.congr_dist

Premises used: Filter.Tendsto.congr_dist
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) atTop (𝓝 0)

Tactic:
IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.ofReal, Asymptotics.IsBigO.trans_tendsto