Theorem: cauchy_dist (Ray/Analytic/Uniform.lean)

State before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ dist ((cauchyPowerSeries f c (↑r) n) fun x => w) ((cauchyPowerSeries g c (↑r) n) fun x => w) ≤
    Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Tactic:
rw [Complex.dist_eq, cauchy_sub n w rp cf cg]
State after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ Complex.abs ((cauchyPowerSeries (f - g) c (↑r) n) fun x => w) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d

State before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ Complex.abs ((cauchyPowerSeries (f - g) c (↑r) n) fun x => w) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Tactic:
refine cauchy_bound rp ?_
State after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ ∀ w ∈ closedBall c ↑r, Complex.abs ((f - g) w) ≤ ↑d

State before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ ∀ w ∈ closedBall c ↑r, Complex.abs ((f - g) w) ≤ ↑d
Tactic:
intro z zr
State after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
z : ℂ
zr : z ∈ closedBall c ↑r
⊢ Complex.abs ((f - g) z) ≤ ↑d

State before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
z : ℂ
zr : z ∈ closedBall c ↑r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Tactic:
simp at h zr
State after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
z : ℂ
h : ∀ (z : ℂ), nndist z c ≤ r → Complex.abs (f z - g z) ≤ ↑d
zr : nndist z c ≤ r
⊢ Complex.abs ((f - g) z) ≤ ↑d

State before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
z : ℂ
h : ∀ (z : ℂ), nndist z c ≤ r → Complex.abs (f z - g z) ≤ ↑d
zr : nndist z c ≤ r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Tactic:
refine h z zr
State after:
no goals