Theorem: cauchy1_hasSum (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : w ∈ ball 0 r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp at wm
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
have ci : CircleIntegrable f c r := ContinuousOn.circleIntegrable (by linarith) fc
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
have h := hasSum_cauchyPowerSeries_integral ci wm
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (cauchyPowerSeries f c r n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (cauchyPowerSeries f c r n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp_rw [cauchyPowerSeries_apply] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
generalize hs : (2*π*I : ℂ)⁻¹ = s
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
h :
  HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
simp_rw [hs] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
Tactic:
generalize hg : (s • ∮ z : ℂ in C(c, r), (z - (c + w))⁻¹ • f z) = g
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
h :
  HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z)
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
rw [hg] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
h : HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) g
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
h : HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) g
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
simp_rw [div_eq_mul_inv, mul_pow, ← smul_smul, circleIntegral.integral_smul, smul_comm s _] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
h : HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
h : HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
assumption
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
f : ℂ → E
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ 0 ≤ r
Tactic:
linarith
State after:
no goals