awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖(↑t : ℂ) * z‖ ≤ ‖1 + (↑t : ℂ) * z‖
have rw : 1 - ‖-((↑t : ℂ) * z)‖ ≤ ‖1 - -((↑t : ℂ) * z)‖
Tactic: rw [← norm_neg (t * z), ← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-((↑t : ℂ) * z)‖ ≤ ‖1 - -((↑t : ℂ) * z)‖
have h : 1 = norm (E := ℂ) 1
Tactic: convert! norm_sub_norm_le 1 (-(t * z))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖
have calc : 1 - ‖z‖ ≤ 1 - t * ‖z‖
Tactic: calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
calc : 1 - ‖z‖ ≤ 1 - t * ‖z‖
⊢ 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖
have calc₁ : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖
Tactic: calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
calc : 1 - ‖z‖ ≤ 1 - t * ‖z‖
calc₁ : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖
⊢ 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖
have calc₂ : 1 - ‖(↑t : ℂ) * z‖ ≤ ‖1 + (↑t : ℂ) * z‖
Tactic: calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖) MeasureTheory.volume 0 1
have this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.Icc 0 1)
Tactic: have := continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.Icc 0 1)
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖) MeasureTheory.volume 0 1
have this₁ : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
Tactic: rw [← Set.uIcc_of_le zero_le_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖) (Set.uIcc 0 1)
have funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.uIcc 0 1) x → 1 + (↑x : ℂ) * z ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
Tactic: have help : IntervalIntegrable (fun t : ℝ ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1 :=
    IntervalIntegrable.mul_const (Continuous.intervalIntegrable (by fun_prop) 0 1) (1 - ‖z‖)⁻¹
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
⊢ HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
have rw : HasDerivAt f (f' ((↑t : ℂ) * z)) ((↑t : ℂ) * z)
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
Tactic: have hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (0 + t * z)) (0 + t * z) := by
    intro t ht
    rw [zero_add]
    exact hasDerivAt_log_sub_logTaylor n <|
      StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
have simp : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' ((↑t : ℂ) * z)) (Set.Icc 0 1)
Tactic: simp only [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
Tactic: have hcont : ContinuousOn (fun t : ℝ ↦ f' (0 + t * z)) (Set.Icc 0 1) := by
    simp only [zero_add]
    exact (Continuous.continuousOn (by fun_prop)).mul <|
      continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ f z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
have h : f z = f (0 + z) - f 0
Tactic: convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
h : f z = f (0 + z) - f 0
⊢ f z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
have h₁ : z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹ =
  HSMul.hSMul (β := ℂ) z (∫ (t : ℝ) in 0..1, f' (0 + t • z))
Tactic: convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have H : f z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
Tactic: have H : f z = z * ∫ t in (0 : ℝ)..1, (-(t * z)) ^ n * (1 + t * z)⁻¹ := by
    convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
    · simp only [f, zero_add, add_zero, log_one, logTaylor_at_zero, sub_self, sub_zero]
    · simp only [f', real_smul, zero_add,
        smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have simp : ‖z‖ * norm (E := ℂ) (∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤
  ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: simp only [H, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ ‖z‖ * norm (E := ℂ) (∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have simp_rw : ‖z‖ ^ (n + 1) * norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤
  ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: simp_rw [neg_pow (_ * z) n, mul_assoc, intervalIntegral.integral_const_mul, mul_pow,
    mul_comm _ (z ^ n), mul_assoc, intervalIntegral.integral_const_mul, norm_mul, norm_pow,
    norm_neg, norm_one, one_pow, one_mul, ← mul_assoc, ← pow_succ', mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ ‖z‖ ^ (n + 1) * norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hbc : norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹
have refine : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
Tactic: refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
t : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
have h : ∀ (ht₀ : 0 < t) (ht₁ : t ≤ 1), ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
Tactic: ⟨ht₀, ht₁⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
have h : ∀ (t : ℝ) (ht₀ : 0 < t) (ht₁ : t ≤ 1), ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
Tactic: filter_upwards with t ⟨ht₀, ht₁⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
have h : t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
Tactic: rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
have h : ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹ = (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rw : (1 - ‖z‖)⁻¹ * ((HPow.hPow (α := ℝ) 1 (n + 1) - HPow.hPow (α := ℝ) 0 (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
⊢ norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc : norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹
Tactic: calc ‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
    _ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ := by
      refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
      filter_upwards with t ⟨ht₀, ht₁⟩
      rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
      gcongr
      exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz
    _ = (1 - ‖z‖)⁻¹ / (n + 1) := by
      rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
      simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
calc : norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹
⊢ norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have calc₁ : ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹ = (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: calc ‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
    _ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ := by
      refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
      filter_upwards with t ⟨ht₀, ht₁⟩
      rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
      gcongr
      exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz
    _ = (1 - ‖z‖)⁻¹ / (n + 1) := by
      rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
      simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2
have h : log (1 + z) - z = log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z
Tactic: convert! norm_log_sub_logTaylor_le 1 hz using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
h : log (1 + z) - z = log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z
⊢ ‖log (1 + z) - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2
have h₁ : 2 = HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
Tactic: convert! norm_log_sub_logTaylor_le 1 hz using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z) fun (z : ℂ) ↦ z ^ (n + 1)
have rw : ∃ (c : ℝ), ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖
Tactic: rw [Asymptotics.isBigO_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖
have h : ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ (n + 1)‖
Tactic: use 2 / (n + 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ (n + 1)‖
have h : ∀ (z : ℂ) (hz1 : ‖z - 0‖ < 1) (hz12 : ‖z - 0‖ < 1 / 2),
  ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
Tactic: filter_upwards [
    eventually_norm_sub_lt 0 one_pos,
    eventually_norm_sub_lt 0 (show 0 < 1 / 2 by simp)] with z hz1 hz12
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
hz12 : ‖z - 0‖ < 1 / 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
have hz1₁ : ‖z‖ < 1
Tactic: rw [sub_zero] at hz1 hz12
Cleared hypotheses: hz1, hz12
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
hz12 : ‖z - 0‖ < 1 / 2
hz1₁ : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
have hz12₁ : ‖z‖ < 1 / 2
Tactic: rw [sub_zero] at hz1 hz12
Cleared hypotheses: hz1, hz12
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2
have rw : 2⁻¹ ≤ 1 - ‖z‖
Tactic: rw [inv_le_comm₀ (sub_pos_of_lt hz1) two_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ 2⁻¹ ≤ 1 - ‖z‖
have linarith : 1 - ‖z‖ < 2⁻¹ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
linarith : 1 - ‖z‖ < 2⁻¹ → 2 / 2 = 1
⊢ 2⁻¹ ≤ 1 - ‖z‖
have linarith₁ : 1 - ‖z‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
linarith : 1 - ‖z‖ < 2⁻¹ → 2 / 2 = 1
linarith₁ : 1 - ‖z‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2⁻¹ ≤ 1 - ‖z‖
have linarith₂ : 1 - ‖z‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
Tactic: linarith