internlm/Lean-Github huggingface dataset:
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
refine
  HasFPowerSeriesOnBall.analyticAt
    { r_le := le_radius_cauchyPowerSeries g c r
      r_pos := ENNReal.coe_pos.mpr rp
      hasSum := ?_ }
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
intro y yb
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have yr := yb
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
simp at yr
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
set a := abs y / r
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a0 : a ≥ 0 := by bound
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a1 : a < 1 := (div_lt_one (NNReal.coe_pos.mpr rp)).mpr yr
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a1p : 1 - a > 0 := by bound
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
rw [HasSum, Metric.tendsto_atTop]
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < ε
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < ε
Tactic:
intro e ep
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
generalize d4 : (1 - a) * (e / 4) = d
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
have dp : d > 0 := by rw [← d4]; bound
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rcases Filter.eventually_atTop.mp (Metric.tendstoUniformlyOn_iff.mp u d dp) with ⟨n, hn'⟩
Proof state after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
set hn := hn' n
Proof state after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : n ≥ n → ∀ x ∈ s, dist (g x) (f n x) < d := hn' n
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : n ≥ n → ∀ x ∈ s, dist (g x) (f n x) < d := hn' n
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
simp at hn
Proof state after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear hn' u
Proof state after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e