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
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
Tactic:
intro z zb
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'
dd : ↑d' = d
z : ℂ
zb : z ∈ closedBall c ↑r
⊢ Complex.abs (g z - f n z) ≤ ↑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'
dd : ↑d' = d
z : ℂ
zb : z ∈ closedBall c ↑r
⊢ Complex.abs (g z - f n z) ≤ ↑d'
Tactic:
exact _root_.trans (hn z (cb zb)).le (le_of_eq dd.symm)
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'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ 0 ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k
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 : ℂ
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
Tactic:
have pgb : (M.sum fun k ↦ a ^ k) ≤ (1 - a)⁻¹ := partial_geometric_bound M a0 a1
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k * d) ≤ e / 4
Tactic:
calc
  (M.sum fun k ↦ a ^ k * d) = (M.sum fun k ↦ a ^ k) * d := by rw [← Finset.sum_mul]
  _ ≤ (1 - a)⁻¹ * d := by bound
  _ = (1 - a)⁻¹ * ((1 - a) * (e / 4)) := by rw [← d4]
  _ = (1 - a) * (1 - a)⁻¹ * (e / 4) := by ring
  _ = 1 * (e / 4) := by rw [mul_inv_cancel a1p.ne']
  _ = e / 4 := by ring
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k * d) = (M.sum fun k => a ^ k) * d
Tactic:
rw [← Finset.sum_mul]
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k) * d ≤ (1 - a)⁻¹ * d
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 : ℂ
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a)⁻¹ * d = (1 - a)⁻¹ * ((1 - a) * (e / 4))
Tactic:
rw [← d4]
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a)⁻¹ * ((1 - a) * (e / 4)) = (1 - a) * (1 - a)⁻¹ * (e / 4)
Tactic:
ring
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a) * (1 - a)⁻¹ * (e / 4) = 1 * (e / 4)
Tactic:
rw [mul_inv_cancel a1p.ne']
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
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ 1 * (e / 4) = e / 4
Tactic:
ring
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 ℕ
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 (f n (c + y)) + dist (f n (c + y)) (g (c + y)) ≤ dist Mp Mpr + dist Mpr (f n (c + y)) + d
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 : ℂ
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 Mpr + dist Mpr (f n (c + y)) + d ≤ e / 4 + d + d
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 : ℂ
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
⊢ e / 4 + d + d = e / 4 + 2 * (1 - a) * (e / 4)
Tactic:
rw [← d4]
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 ℕ
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
⊢ e / 4 + (1 - a) * (e / 4) + (1 - a) * (e / 4) = e / 4 + 2 * (1 - a) * (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 ℕ
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
⊢ e / 4 + (1 - a) * (e / 4) + (1 - a) * (e / 4) = e / 4 + 2 * (1 - a) * (e / 4)
Tactic:
ring
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 ℕ
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
⊢ e / 4 + 2 * (1 - a) * (e / 4) ≤ e / 4 + 2 * (1 - 0) * (e / 4)
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 : ℂ
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
⊢ e / 4 + 2 * (1 - 0) * (e / 4) = 3 / 4 * e
Tactic:
ring
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 ℕ
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
⊢ 3 / 4 < 1
Tactic:
norm_num
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 ℕ
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
⊢ 1 * e = e
Tactic:
simp
Proof state after:
no goals
Theorem: pow_mul_nat
Proof state before:
z w : ℂ
n : ℕ
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
simp only [Complex.cpow_def_of_ne_zero z0, ← Complex.exp_nat_mul]
Proof state after:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (↑n * (z.log * w)).exp = (z.log * (w * ↑n)).exp
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (↑n * (z.log * w)).exp = (z.log * (w * ↑n)).exp
Tactic:
ring_nf
Proof state after:
no goals
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
rw [z0]
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
by_cases w0 : w = 0
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
have wn0 : w * n ≠ 0 := mul_ne_zero w0 (Nat.cast_ne_zero.mpr n0)
Proof state after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [Complex.zero_cpow w0]
Proof state after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0 ^ (w * ↑n)
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0 ^ (w * ↑n)
Tactic:
rw [Complex.zero_cpow wn0]
Proof state after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0
Theorem: pow_mul_nat
Proof state before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0
Tactic:
exact zero_pow n0
Proof state after:
no goals
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [w0]
Proof state after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ 0) ^ n = 0 ^ (0 * ↑n)
Theorem: pow_mul_nat
Proof state before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ 0) ^ n = 0 ^ (0 * ↑n)
Tactic:
simp
Proof state after:
no goals