Theorem: unevenTerm_eq (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
⊢ z1 ∈ closedBall c1 r1 → unevenTerm' u r z1 = unevenTerm u z1
Tactic:
intro z1s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenTerm' u r z1 = unevenTerm u z1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenTerm' u r z1 = unevenTerm u z1
Tactic:
funext x
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have p0 := u.has_series rp rr1 z1s
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have p1 := u.has_series u.r1p (by rfl) z1s
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
have h := HasFPowerSeriesAt.eq_formalMultilinearSeries p0.hasFPowerSeriesAt p1.hasFPowerSeriesAt
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
p1 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r1 z1) c0 (ENNReal.ofReal r1)
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
clear p0 p1
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
h : unevenSeries' u r z1 = unevenSeries' u r1 z1
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x
Tactic:
simp only [unevenTerm, ←unevenSeries_apply, h]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
p0 : HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u r z1) c0 (ENNReal.ofReal r)
⊢ r1 ≤ r1
Tactic:
rfl
State after:
no goals