internlm/Lean-Github huggingface dataset:
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have pa := (p.hasFPowerSeriesOnBall_changeOrigin n (lt_of_lt_of_le hp.r_pos hp.r_le)).analyticAt
Proof state after:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
set g := fun w1 ↦ ((0 : ℂ), w1 - z1)
Proof state after:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have ga : AnalyticOn ℂ g univ := by
  rw [analyticOn_univ_iff_differentiable]
  exact (differentiable_const _).prod (differentiable_id.sub (differentiable_const _))
Proof state after:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have g0 : 0 = g z1 := by
  simp only [Prod.ext_iff, Prod.fst_zero, Prod.snd_zero, sub_self, and_self_iff]
Proof state after:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rw [g0] at pa
Proof state after:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have ta := pa.comp (ga z1 (Set.mem_univ _))
Proof state after:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ ((fun x => p.changeOrigin x n) ∘ g) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ ((fun x => p.changeOrigin x n) ∘ g) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
simp_rw [Function.comp] at ta
Proof state after:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
clear pa ga g0
Proof state after:
case intro.intro
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
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rw [analyticAt_congr pu]
Proof state after:
case intro.intro
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
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun x => (p.changeOrigin (g x)).along0 n) z1
Theorem: unevenSeries_analytic
Proof state before:
case intro.intro
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
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun x => (p.changeOrigin (g x)).along0 n) z1
Tactic:
exact (Along0.analyticAt _).comp ta
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticOn ℂ g univ
Tactic:
rw [analyticOn_univ_iff_differentiable]
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ Differentiable ℂ g
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ Differentiable ℂ g
Tactic:
exact (differentiable_const _).prod (differentiable_id.sub (differentiable_const _))
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
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ 0 = g z1
Tactic:
simp only [Prod.ext_iff, Prod.fst_zero, Prod.snd_zero, sub_self, and_self_iff]
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
⊢ ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
rw [eventually_nhds_iff]
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
set s' := r1 - dist z1 c1
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
set s := min r (ENNReal.ofReal s')
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')
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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')
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have s'p : s' > 0 := by simp only [Metric.mem_ball] at z1s; bound
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sp : s > 0 := by bound
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sr : s ≤ r := by bound
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
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
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sb : EMetric.ball z1 s ⊆ ball c1 r1 := by
  rw [Set.subset_def]; intro x xs
  simp only [Metric.mem_ball, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢
  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:
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