internlm/Lean-Github huggingface dataset:
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
use EMetric.ball z1 s
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ (∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧
    IsOpen (EMetric.ball z1 s) ∧ z1 ∈ EMetric.ball z1 s
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ (∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧
    IsOpen (EMetric.ball z1 s) ∧ z1 ∈ EMetric.ball z1 s
Tactic:
refine ⟨?_, EMetric.isOpen_ball, EMetric.mem_ball_self sp⟩
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n
Tactic:
intro w1 w1s
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
have p0 : HasFPowerSeriesAt (fun z0 ↦ f (z0, w1)) (unevenSeries u w1) c0 := by
  have w1c : w1 ∈ closedBall c1 r1 := mem_open_closed (sb w1s)
  refine (Uneven.has_series u u.r1p (le_refl _) w1c).hasFPowerSeriesAt
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
p1 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
rw [HasFPowerSeriesAt.eq_formalMultilinearSeries p0 p1]
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
⊢ s' > 0
Tactic:
simp only [Metric.mem_ball] at z1s
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
z1s : dist z1 c1 < r1
⊢ s' > 0
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
z1s : dist z1 c1 < r1
⊢ s' > 0
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
⊢ s > 0
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
⊢ s ≤ r
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ EMetric.ball z1 s ⊆ ball c1 r1
Tactic:
rw [Set.subset_def]
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∀ x ∈ EMetric.ball z1 s, x ∈ ball c1 r1
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∀ x ∈ EMetric.ball z1 s, x ∈ ball c1 r1
Tactic:
intro x xs
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : x ∈ EMetric.ball z1 s
⊢ x ∈ ball c1 r1
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : x ∈ EMetric.ball z1 s
⊢ x ∈ ball c1 r1
Tactic:
simp only [Metric.mem_ball, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 < r1
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 < r1
Tactic:
calc dist x c1
  _ ≤ dist x z1 + dist z1 c1 := by bound
  _ < s' + dist z1 c1 := (add_lt_add_right xs.right _)
  _ = r1 - dist z1 c1 + dist z1 c1 := rfl
  _ = r1 := by ring_nf
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 ≤ dist x z1 + dist z1 c1
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ r1 - dist z1 c1 + dist z1 c1 = r1
Tactic:
ring_nf
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
Tactic:
have w1c : w1 ∈ closedBall c1 r1 := mem_open_closed (sb w1s)
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
w1c : w1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
w1c : w1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
Tactic:
refine (Uneven.has_series u u.r1p (le_refl _) w1c).hasFPowerSeriesAt
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
Tactic:
have wz : ↑‖((0 : ℂ), w1 - z1)‖₊ < r := by
  simp only [EMetric.mem_ball, edist_dist, Complex.dist_eq] at w1s
  simp only [Prod.nnnorm_def', nnnorm_zero, max_eq_right, zero_le', ← edist_eq_coe_nnnorm,
    edist_dist, Complex.dist_eq, sub_zero]
  exact lt_of_lt_of_le w1s sr
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
Theorem: unevenSeries_analytic
Proof 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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
Tactic:
convert (hp.changeOrigin wz).hasFPowerSeriesAt.along0
Proof state after:
case h.e'_9.h.h.e'_1.h.e'_4
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
x✝ : ℂ
⊢ w1 = (c0, z1).2 + (0, w1 - z1).2

case h.e'_11
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ c0 = (c0, z1).1 + (0, w1 - z1).1