Theorem: Uneven.has_series (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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
set sn := s.toNNReal
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
have sns : s = sn := by simp only [Real.coe_toNNReal', sp.le, max_eq_left, sn]
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
have snp : sn > 0 := Real.toNNReal_pos.mpr sp
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
rw [uneven_is_cauchy]
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 s) c0 (ENNReal.ofReal s)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 s) c0 (ENNReal.ofReal s)
Tactic:
rw [sns, ← ENNReal.coe_nnreal_eq]
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 ↑sn) c0 ↑sn

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 ↑sn) c0 ↑sn
Tactic:
refine DifferentiableOn.hasFPowerSeriesOnBall ?_ snp
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 ↑sn)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 ↑sn)
Tactic:
rw [← sns]
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 s)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 s)
Tactic:
refine DifferentiableOn.mono ?_ (Metric.closedBall_subset_closedBall sr1)
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r1)

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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r1)
Tactic:
exact AnalyticOn.differentiableOn (u.h.on0 z1s)
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
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ s = ↑sn
Tactic:
simp only [Real.coe_toNNReal', sp.le, max_eq_left, sn]
State after:
no goals