awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
h : (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
convert_1 : z ≠ w → id z - w ≠ 0
convert_2 : -1 ≤ n → 0 ≤ n + 1
⊢ HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z

Tactic:
convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1

Premises used: HasDerivAt.comp, HasDerivAt.sub_const, hasDerivAt_id, HAdd.hAdd, HasDerivAt.div_const, Or.imp, OfNat.ofNat, hasDerivAt_zpow
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
rwa : ¬HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0
rwa₁ : ¬Eq (α := ℂ) (↑n : ℂ) (-1)
rwa₂ : ¬Eq (α := ℂ) (↑n : ℂ) (-(↑1 : ℂ))
rwa₃ : ¬Eq (α := ℂ) (↑n : ℂ) (↑(-1) : ℂ)
rwa₄ rwa₅ rwa₆ rwa₇ : ¬n = -1
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]

Premises used: Int.cast_neg, Int.cast_inj, Ne, eq_neg_iff_add_eq_zero, Int.cast_one
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
hn' : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ (z - w) ^ n = (↑(n + 1) : ℂ) * (id z - w) ^ (n + 1 - 1) * 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1

Tactic:
simp [mul_div_cancel_left₀ _ hn']

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0

Tactic:
sub_ne_zero.2

Premises used: Iff.mpr, sub_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ -1 ≤ n → 0 ≤ n + 1

Tactic:
neg_le_iff_add_nonneg.1

Premises used: neg_le_iff_add_nonneg, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0

Tactic:
exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]

Premises used: Iff.mpr, sub_ne_zero, neg_le_iff_add_nonneg, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
⊢ ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z

Tactic:
have hd : ∀ z, z ≠ w ∨ -1 ≤ n →
      HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z := by
    intro z hne
    convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
    · have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
      simp [mul_div_cancel_left₀ _ hn']
    exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
hd :
  ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, circleIntegral.integral_eq_zero_of_hasDerivWithinAt'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
hd :
  ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
neg : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), z ≠ w ∨ -1 ≤ n
⊢ Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - w) ^ n) 0

Tactic:
refine integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, circleIntegral.integral_eq_zero_of_hasDerivWithinAt'
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
hd :
  ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c |R|
⊢ z ≠ w ∨ -1 ≤ n

Tactic:
(ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz

Premises used: ne_or_eq, Eq.rec, Or.imp_right
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ∀ (_ : w ∈ sphere c |R|), -1 ≤ n
hd :
  ∀ (z : ℂ),
    z ≠ w ∨ -1 ≤ n → HasDerivAt (fun (z : ℂ) ↦ (z - w) ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c |R|
⊢ z ≠ w ∨ -1 ≤ n

Tactic:
exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz

Premises used: ne_or_eq, Eq.rec, Or.imp_right
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
simp :
  w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * (↑π : ℂ) * I)⁻¹ • HSMul.hSMul (β := E) (w ^ n) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
⊢ ((cauchyPowerSeries f c R n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w) =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)

Tactic:
simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const,
    div_eq_mul_inv, mul_pow, mul_smul, circleIntegral.integral_smul]

Premises used: ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const, div_eq_mul_inv, circleIntegral.integral_smul, mul_pow, SemigroupAction.mul_smul, cauchyPowerSeries
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
rw rw₁ :
  w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
⊢ w ^ n • HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * (↑π : ℂ) * I)⁻¹ • HSMul.hSMul (β := E) (w ^ n) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)

Tactic:
rw [← smul_comm (w ^ n)]

Premises used: HPow.hPow, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c R n) =
    (2 * π)⁻¹ * norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)

Tactic:
simp [cauchyPowerSeries, norm_smul, Real.pi_pos.le]

Premises used: norm_smul, Real.pi_pos, LT.lt.le, cauchyPowerSeries
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hbc :
  norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) ≤
    ∫ (θ : ℝ) in 0..2 * π,
      ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖
⊢ (2 * π)⁻¹ * norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) ≤
    (2 * π)⁻¹ *
      ∫ (θ : ℝ) in 0..2 * π,
        ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ 0 ≤ 2 * π

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ norm.{u_1} (E := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) ≤
    ∫ (θ : ℝ) in 0..2 * π,
      ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖

Tactic:
exact intervalIntegral.norm_integral_le_integral_norm (by positivity)

Premises used: intervalIntegral.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
⊢ (2 * π)⁻¹ *
      ∫ (θ : ℝ) in 0..2 * π,
        ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖ =
    (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖)))

Tactic:
simp [norm_smul, mul_left_comm |R|]

Premises used: norm_smul, abs, mul_left_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
inl :
  (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n
inr :
  ∀ (hR : R ≠ 0),
    (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
      ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n

Tactic:
rcases eq_or_ne R 0 with (rfl | hR)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
n : ℕ
inl :
  (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0 *
        (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0
inl₁ :
  ∀ (n : ℕ),
    (2 * π)⁻¹ *
        (HPow.hPow (α := ℝ) |0|⁻¹ (n + 1) *
          (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
      ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ (n + 1)
⊢ (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ n * (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ n

Tactic:
cases n
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
⊢ (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0 *
        (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) (β := ℕ) |0|⁻¹ 0

Tactic:
simp [-mul_inv_rev]

Premises used: mul_inv_rev
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
n : ℕ
⊢ (2 * π)⁻¹ *
      (HPow.hPow (α := ℝ) |0|⁻¹ (n + 1) *
        (|0| * HMul.hMul (α := ℝ) |0|⁻¹ (∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * HPow.hPow (α := ℝ) |0|⁻¹ (n + 1)

Tactic:
simp [-mul_inv_rev]

Premises used: mul_inv_rev
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
inr : |R| ≠ 0
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n

Tactic:
rw [mul_inv_cancel_left₀, mul_assoc, mul_comm (|R|⁻¹ ^ n)]

Premises used: mul_inv_cancel_left₀, abs, mul_assoc, Inv.inv, HPow.hPow, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
inr : ¬|R| = 0
inr₁ inr₂ inr₃ inr₄ : ¬R = 0
⊢ |R| ≠ 0

Tactic:
rwa [Ne, _root_.abs_eq_zero]

Premises used: Ne, abs_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
⊢ (↑R : ENNReal) ≤ FormalMultilinearSeries.radius (cauchyPowerSeries f c (↑R : ℝ))

Tactic:
(cauchyPowerSeries f c R).le_radius_of_bound
      ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) fun n => ?_

Premises used: Norm.norm, Real.pi, HMul.hMul, intervalIntegral, circleMap, FormalMultilinearSeries.le_radius_of_bound, Inv.inv, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, NNReal.toReal, cauchyPowerSeries
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
f₁ :
  ∀ (n : ℕ),
    norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c (↑R : ℝ) n) * (↑R : ℝ) ^ n ≤
      (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ (↑R : ENNReal) ≤ FormalMultilinearSeries.radius (cauchyPowerSeries f c (↑R : ℝ))

Tactic:
refine
    (cauchyPowerSeries f c R).le_radius_of_bound
      ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) fun n => ?_

Premises used: Norm.norm, Real.pi, HMul.hMul, intervalIntegral, circleMap, FormalMultilinearSeries.le_radius_of_bound, Inv.inv, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, NNReal.toReal, cauchyPowerSeries
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c (↑R : ℝ) n) * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
(mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _)
    (pow_nonneg R.coe_nonneg _)).trans ?_

Premises used: pow_nonneg, norm_cauchyPowerSeries_le, mul_le_mul_of_nonneg_right, NNReal.coe_nonneg, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
refine :
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * |(↑R : ℝ)|⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) E) (cauchyPowerSeries f c (↑R : ℝ) n) * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
refine (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _)
    (pow_nonneg R.coe_nonneg _)).trans ?_

Premises used: pow_nonneg, norm_cauchyPowerSeries_le, mul_le_mul_of_nonneg_right, NNReal.coe_nonneg, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
rw :
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * |(↑R : ℝ)|⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
rw [abs_of_nonneg R.coe_nonneg]

Premises used: NNReal.coe_nonneg, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
inl :
  ∀ (hR : (↑R : ℝ) ^ n = 0),
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
      (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
inr :
  ∀ (hR : (↑R : ℝ) ^ n ≠ 0),
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
      (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
rcases eq_or_ne (R ^ n : ℝ) 0 with hR | hR

Premises used: HPow.hPow, eq_or_ne, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n = 0
inl : ∀ (hR : R ^ n = 0), 0 ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
rw_mod_cast [hR, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : R ^ n = 0
⊢ 0 ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
      (intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)

Premises used: Iff.mpr, mul_nonneg, circleMap, LT.lt.le, Real.two_pi_pos, inv_nonneg, NNReal.toReal, norm_nonneg, intervalIntegral.integral_nonneg
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : R ^ n = 0
⊢ 0 ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
exact mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
      (intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)

Premises used: Iff.mpr, mul_nonneg, LT.lt.le, Real.two_pi_pos, inv_nonneg, norm_nonneg, intervalIntegral.integral_nonneg
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n ≠ 0
inr :
  ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * ((↑R : ℝ) ^ n)⁻¹ * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * (↑R : ℝ)⁻¹ ^ n * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
rw [inv_pow]

Premises used: inv_pow
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (hR : ¬R ^ n = 0), ¬R ^ n = 0
⊢ (↑R : ℝ) ^ n ≠ 0

Tactic:
norm_cast at hR ⊢
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : (↑R : ℝ) ^ n ≠ 0
⊢ (↑R : ℝ) ^ n ≠ 0

Tactic:
have : (R : ℝ) ^ n ≠ 0 := by norm_cast at hR ⊢
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR this : (↑R : ℝ) ^ n ≠ 0
inr inr₁ :
  (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖ ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖) * ((↑R : ℝ) ^ n)⁻¹ * (↑R : ℝ) ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R : ℝ) θ)‖

Tactic:
rw [inv_mul_cancel_right₀ this]

Premises used: inv_mul_cancel_right₀
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ 0 < R

Tactic:
have hR : 0 < R := (norm_nonneg w).trans_lt hw
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)

Tactic:
have hwR : ‖w‖ / R ∈ Ico (0 : ℝ) 1 :=
    ⟨div_nonneg (norm_nonneg w) hR.le, (div_lt_one hR).2 hw⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
intervalIntegral.hasSum_integral_of_dominated_convergence
      (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) (fun n => ?_) (fun n => ?_) ?_ ?_ ?_

Premises used: Norm.norm, HMul.hMul, circleMap, HDiv.hDiv, HPow.hPow, intervalIntegral.hasSum_integral_of_dominated_convergence, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
      (fun (θ : ℝ) ↦
        HSMul.hSMul (β := E) (deriv (circleMap c R) θ)
          ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ)))
      (Measure.restrict volume (Ι 0 (2 * π)))
refine_2 :
  ∀ (n : ℕ),
    ∀ᵐ (t : ℝ),
      t ∈ Ι 0 (2 * π) →
        ‖HSMul.hSMul (β := E) (deriv (circleMap c R) t)
              ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))‖ ≤
          (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t
refine_3 :
  ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) → Summable (α := ℝ) fun (n : ℕ) ↦ (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t
refine_4 :
  IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦ ∑' (n : ℕ), (fun (n : ℕ) (θ : ℝ) ↦ ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) n t) volume 0 (2 * π)
refine_5 :
  ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum
        (fun (n : ℕ) ↦
          HSMul.hSMul (β := E) (deriv (circleMap c R) t)
            ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)))
        (HSMul.hSMul (β := E) (deriv (circleMap c R) t) ((fun (z : ℂ) ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t)))
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
refine intervalIntegral.hasSum_integral_of_dominated_convergence
      (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) (fun n => ?_) (fun n => ?_) ?_ ?_ ?_

Premises used: Norm.norm, HMul.hMul, circleMap, HDiv.hDiv, HPow.hPow, intervalIntegral.hasSum_integral_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : Membership.mem (γ := Set ℝ) (Ico 0 1) (‖w‖ / R)
n : ℕ
refine_1 :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦
      (circleMap 0 R θ * I) • (w / (circleMap c R θ - c)) ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ))
    (Measure.restrict volume (Ι 0 (2 * π)))
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := Real.measurableSpace)
    (fun (θ : ℝ) ↦
      HSMul.hSMul (β := E) (deriv (circleMap c R) θ)
        ((fun (z : ℂ) ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ)))
    (Measure.restrict volume (Ι 0 (2 * π)))

Tactic:
simp only [deriv_circleMap]

Premises used: deriv_circleMap