internlm/Lean-Github huggingface dataset:
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) ≤
    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
Tactic:
apply dist_sum_sum_le M (fun k : ℕ ↦ p k fun _ ↦ y) fun k : ℕ ↦ 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
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4
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
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4
Tactic:
trans M.sum fun k ↦ a ^ k * d
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
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ M.sum fun k => a ^ k * d

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 => a ^ k * d) ≤ e / 4
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
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ M.sum fun k => a ^ k * d
Tactic:
apply Finset.sum_le_sum
Proof state after:
case h
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
⊢ ∀ i ∈ M, dist ((p i) fun x => y) ((pr n i) fun x => y) ≤ a ^ i * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
⊢ ∀ i ∈ M, dist ((p i) fun x => y) ((pr n i) fun x => y) ≤ a ^ i * d
Tactic:
intro k _
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Tactic:
have hak : a ^ k = abs y ^ k * r⁻¹ ^ k := by
  calc (abs y / r) ^ k
    _ = (abs y * r⁻¹) ^ k := by rw [div_eq_mul_inv, NNReal.coe_inv]
    _ = abs y ^ k * r⁻¹ ^ k := mul_pow _ _ _
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Tactic:
rw [hak]
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
generalize hd' : d.toNNReal = d'
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
have dd : (d' : ℝ) = d := by rw [← hd']; exact Real.coe_toNNReal d dp.le
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
have hcb : ∀ z, z ∈ closedBall c r → abs (g z - f n z) ≤ d' := by
  intro z zb; exact _root_.trans (hn z (cb zb)).le (le_of_eq dd.symm)
Proof state after:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Theorem: uniform_analytic_lim
Proof state before:
case h
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
exact _root_.trans (cauchy_dist k y rp cg (cf n) hcb)
  (mul_le_mul_of_nonneg_left (le_of_eq dd) (by 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 : ℂ
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
k : ℕ
a✝ : k ∈ M
⊢ a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
Tactic:
calc (abs y / r) ^ k
  _ = (abs y * r⁻¹) ^ k := by rw [div_eq_mul_inv, NNReal.coe_inv]
  _ = abs y ^ k * r⁻¹ ^ k := mul_pow _ _ _
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
k : ℕ
a✝ : k ∈ M
⊢ (Complex.abs y / ↑r) ^ k = (Complex.abs y * ↑r⁻¹) ^ k
Tactic:
rw [div_eq_mul_inv, NNReal.coe_inv]
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d' = d
Tactic:
rw [← hd']
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d.toNNReal = d
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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d.toNNReal = d
Tactic:
exact Real.coe_toNNReal d dp.le
Proof state after:
no goals