internlm/Lean-Github huggingface dataset:
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
Mpr : ℂ
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e
Tactic:
rw [hMpr] at dpf 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 ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ 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 ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e
Tactic:
calc dist Mp (g (c + y))
  _ ≤ dist Mp (f n (c + y)) + dist (f n (c + y)) (g (c + y)) := dist_triangle _ _ _
  _ ≤ dist Mp Mpr + dist Mpr (f n (c + y)) + d := by bound
  _ ≤ e / 4 + d + d := by bound
  _ = e / 4 + 2 * (1 - a) * (e / 4) := by rw [← d4]; ring
  _ ≤ e / 4 + 2 * (1 - 0) * (e / 4) := by bound
  _ = 3 / 4 * e := by ring
  _ < 1 * e := (mul_lt_mul_of_pos_right (by norm_num) ep)
  _ = e := by simp
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
intro n
Proof state after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
have cs := cauchy_on_cball_radius rp (hb n)
Proof state after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
have pn : pr n = cauchyPowerSeries (f n) c r := rfl
Proof state after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
rw [← pn] at cs
Proof state after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (pr n) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (pr n) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
exact cs
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
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
⊢ a ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
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
⊢ 1 - a > 0
Tactic:
bound
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
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
⊢ d > 0
Tactic:
rw [← d4]
Proof state after:
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
⊢ (1 - a) * (e / 4) > 0
Theorem: uniform_analytic_lim
Proof state before:
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
⊢ (1 - a) * (e / 4) > 0
Tactic:
bound
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
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
⊢ dist (f n (c + y)) (g (c + y)) ≤ d
Tactic:
apply le_of_lt
Proof state after:
case a
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
⊢ dist (f n (c + y)) (g (c + y)) < d
Theorem: uniform_analytic_lim
Proof state before:
case a
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
⊢ dist (f n (c + y)) (g (c + y)) < d
Tactic:
rw [dist_comm]
Proof state after:
case a
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
⊢ dist (g (c + y)) (f n (c + y)) < d
Theorem: uniform_analytic_lim
Proof state before:
case a
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
⊢ dist (g (c + y)) (f n (c + y)) < d
Tactic:
refine hn (c + y) ?_
Proof state after:
case a
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
⊢ c + y ∈ s
Theorem: uniform_analytic_lim
Proof state before:
case a
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
⊢ c + y ∈ s
Tactic:
apply cb
Proof state after:
case a.a
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
⊢ c + y ∈ closedBall c ↑r
Theorem: uniform_analytic_lim
Proof state before:
case a.a
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
⊢ c + y ∈ closedBall c ↑r
Tactic:
simp
Proof state after:
case a.a
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
⊢ Complex.abs y ≤ ↑r
Theorem: uniform_analytic_lim
Proof state before:
case a.a
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
⊢ Complex.abs y ≤ ↑r
Tactic:
exact yr.le
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
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 k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Tactic:
trans M.sum fun k : ℕ ↦ dist (p k fun _ ↦ y) (pr n k fun _ ↦ y)
Proof state after:
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 k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤
    M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)

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
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4