Theorem: cauchy_sub (Ray/Analytic/Uniform.lean)

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((cauchyPowerSeries f c (↑r) n) fun x => w) - (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply f c r n w]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply g c r n w]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply (f - g) c r n w]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z
Tactic:
set s : ℂ := (2 * π * I)⁻¹
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z
Tactic:
simp only [div_pow, Algebra.id.smul_eq_mul, Pi.sub_apply]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have fi := cauchy_is_circleIntegrable n w rp cf
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have gi := cauchy_is_circleIntegrable n w rp cg
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have cia := circleIntegral_sub fi gi
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
rw [← mul_sub_left_distrib, cia]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
clear cia fi gi cf cg rp
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have flip :
  ((fun z ↦ w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z ↦
      w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    fun z ↦ w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z) :=
  rfl
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
flip :
  ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) = fun z =>
    w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
flip :
  ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) = fun z =>
    w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
simp only [flip, mul_sub_left_distrib]
State after:
no goals