-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The difference of `log (1+z)` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`. -/
lemma norm_log_sub_logTaylor_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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)⁻¹
⊢ ‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
calc ‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
  _ ≤ ∫ t in (0 : ℝ)..1, ‖(t : ℂ) ^ n * (1 + t * z)⁻¹‖ :=
      intervalIntegral.norm_integral_le_integral_norm zero_le_one
  _ = ∫ t in (0 : ℝ)..1, t ^ n * ‖(1 + t * z)⁻¹‖ := by
      refine intervalIntegral.integral_congr <| fun t ht ↦ ?_
      rw [Set.uIcc_of_le zero_le_one, Set.mem_Icc] at ht
      simp_rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht.1]
  _ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ :=
      intervalIntegral.integral_mono_on zero_le_one
        (integrable_pow_mul_norm_one_add_mul_inv n hz) help <|
        fun t ht ↦ mul_le_mul_of_nonneg_left (norm_one_add_mul_inv_le ht hz)
                     (pow_nonneg ((Set.mem_Icc.mp ht).1) _)
  _ = (1 - ‖z‖)⁻¹ / (n + 1) := by
      rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
      field_simp

Result:
no goals

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
let f' (z : ℂ) : ℂ := (-z) ^ n * (1 + z)⁻¹

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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‖)⁻¹ / (↑n + 1)

Tactic:
rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ((1 ^ (n + 1) - 0 ^ (n + 1)) / (↑n + 1)) = (1 - ‖z‖)⁻¹ / (↑n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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‖ * ‖∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑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]

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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) * ‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / (↑n + 1))

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
have hcont : ContinuousOn (fun t : ℝ ↦ f' (0 + t * z)) (Set.Icc 0 1) := by
  simp only [zero_add, zero_le_one, not_true_eq_false]
  exact (Continuous.continuousOn (by fun_prop)).mul <|
    continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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) * ‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / (↑n + 1))

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (norm_nonneg z) (n + 1))

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (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)⁻¹
⊢ ‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹ / (↑n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
⊢ ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)

Tactic:
intro t ht

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)