internlm/Lean-Github huggingface dataset:
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 ℂ
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
Tactic:
have dfg : dist (f n (c + y)) (g (c + y)) ≤ d := by
  apply le_of_lt; rw [dist_comm]
  refine hn (c + y) ?_
  apply cb
  simp; exact yr.le
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ 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 ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
set hs := (hpf n).hasSum yb
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : HasSum (fun n_1 => (pr n n_1) fun x => y) (f n (c + y)) := (hpf n).hasSum yb
⊢ ∃ 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 ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : HasSum (fun n_1 => (pr n n_1) fun x => y) (f n (c + y)) := (hpf n).hasSum yb
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rw [HasSum, Metric.tendsto_atTop] at hs
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
⊢ ∃ 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 ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rcases hs d dp with ⟨N, NM⟩
Proof state after:
case intro.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < 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.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear hs
Proof state after:
case intro.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < 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.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
exists N
Proof state after:
case intro.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∀ 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.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
intro M NlM
Proof state after:
case intro.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
⊢ dist (M.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.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
have dpf := (NM M NlM).le
Proof state after:
case intro.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.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.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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear NM NlM N yb
Proof state after:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.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.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
generalize hMp : M.sum (fun k : ℕ ↦ p k fun _ ↦ y) = Mp
Proof state after:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Tactic:
rw [hMp] at dppr
Proof state after:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Theorem: uniform_analytic_lim
Proof state before:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Tactic:
generalize hMpr : M.sum (fun k ↦ pr n k fun _ ↦ y) = Mpr
Proof state after:
case intro.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 : ℂ
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
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e