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

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
⊢ Complex.abs ((cauchyPowerSeries f c (↑r) n) fun x => w) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Tactic:
set wr := abs w ^ n * r⁻¹ ^ n * d
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
⊢ Complex.abs ((cauchyPowerSeries f c (↑r) n) fun x => w) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
⊢ Complex.abs ((cauchyPowerSeries f c (↑r) n) fun x => w) ≤ wr
Tactic:
rw [cauchyPowerSeries_apply f c r n w, smul_eq_mul, Complex.abs.map_mul]
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) ≤ wr
Tactic:
generalize hg : (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
have gs : ∀ z ∈ sphere c r, ‖g z‖ ≤ wr * r⁻¹ := by
  intro z; simp only [mem_sphere_iff_norm, Complex.norm_eq_abs]; intro zr
  simp only [← hg, zr, div_pow, Algebra.id.smul_eq_mul, AbsoluteValue.map_mul, map_div₀,
    Complex.abs_pow, map_inv₀]
  have zb : z ∈ closedBall c r := by
    simp only [Metric.mem_closedBall, dist_le_coe, ← NNReal.coe_le_coe, coe_nndist,
      Complex.dist_eq, zr, le_refl]
  have zs := h z zb
  calc abs w ^ n / ↑r ^ n * (r⁻¹ * abs (f z))
    _ = abs w ^ n * (r⁻¹ ^ n : ℝ≥0) * (r⁻¹ * abs (f z)) := by
      rw [div_eq_mul_inv, ← inv_pow, NNReal.coe_pow, NNReal.coe_inv]
    _ ≤ abs w ^ n * r⁻¹ ^ n * (r⁻¹ * d) := by bound
    _ = abs w ^ n * r⁻¹ ^ n * d * r⁻¹ := by ring
    _ = wr * r⁻¹ := rfl
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
have cn := circleIntegral.norm_integral_le_of_norm_le_const (NNReal.coe_nonneg r) gs
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : ‖∮ (z : ℂ) in C(c, ↑r), g z‖ ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : ‖∮ (z : ℂ) in C(c, ↑r), g z‖ ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
rw [Complex.norm_eq_abs] at cn
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
⊢ Complex.abs (2 * ↑π * I)⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
simp only [mul_inv_rev, Complex.inv_I, AbsoluteValue.map_neg, AbsoluteValue.map_mul,
  Complex.abs_I, map_inv₀, Complex.abs_ofReal, Complex.abs_two, one_mul, div_pow,
  Algebra.id.smul_eq_mul] at hg cn ⊢
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
⊢ |π|⁻¹ * 2⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
⊢ |π|⁻¹ * 2⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
have p3 : |π| = π := abs_eq_self.mpr (by bound)
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ |π|⁻¹ * 2⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ |π|⁻¹ * 2⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ wr
Tactic:
calc |π|⁻¹ * 2⁻¹ * abs (circleIntegral g c ↑r)
  _ ≤ |π|⁻¹ * 2⁻¹ * (2 * π * r * (wr * r⁻¹)) := by bound
  _ = π * |π|⁻¹ * (r * r⁻¹) * wr := by ring
  _ = π * π⁻¹ * (r * r⁻¹) * wr := by rw [p3]
  _ = 1 * (r * r⁻¹) * wr := by rw [mul_inv_cancel Real.pi_ne_zero]
  _ = wr := by
    rw [NNReal.coe_inv, mul_inv_cancel (NNReal.coe_ne_zero.mpr rp.ne'), one_mul, one_mul]
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
⊢ ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
Tactic:
intro z
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
⊢ z ∈ sphere c ↑r → ‖g z‖ ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
⊢ z ∈ sphere c ↑r → ‖g z‖ ≤ wr * ↑r⁻¹
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs]
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
⊢ Complex.abs (z - c) = ↑r → Complex.abs (g z) ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
⊢ Complex.abs (z - c) = ↑r → Complex.abs (g z) ≤ wr * ↑r⁻¹
Tactic:
intro zr
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
⊢ Complex.abs (g z) ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
⊢ Complex.abs (g z) ≤ wr * ↑r⁻¹
Tactic:
simp only [← hg, zr, div_pow, Algebra.id.smul_eq_mul, AbsoluteValue.map_mul, map_div₀,
  Complex.abs_pow, map_inv₀]
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹
Tactic:
have zb : z ∈ closedBall c r := by
  simp only [Metric.mem_closedBall, dist_le_coe, ← NNReal.coe_le_coe, coe_nndist,
    Complex.dist_eq, zr, le_refl]
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹
Tactic:
have zs := h z zb
State after:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
zs : Complex.abs (f z) ≤ ↑d
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
zs : Complex.abs (f z) ≤ ↑d
⊢ Complex.abs w ^ n / ↑r ^ n * ((↑r)⁻¹ * Complex.abs (f z)) ≤ wr * ↑r⁻¹
Tactic:
calc abs w ^ n / ↑r ^ n * (r⁻¹ * abs (f z))
  _ = abs w ^ n * (r⁻¹ ^ n : ℝ≥0) * (r⁻¹ * abs (f z)) := by
    rw [div_eq_mul_inv, ← inv_pow, NNReal.coe_pow, NNReal.coe_inv]
  _ ≤ abs w ^ n * r⁻¹ ^ n * (r⁻¹ * d) := by bound
  _ = abs w ^ n * r⁻¹ ^ n * d * r⁻¹ := by ring
  _ = wr * r⁻¹ := rfl
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
⊢ z ∈ closedBall c ↑r
Tactic:
simp only [Metric.mem_closedBall, dist_le_coe, ← NNReal.coe_le_coe, coe_nndist,
  Complex.dist_eq, zr, le_refl]
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
zs : Complex.abs (f z) ≤ ↑d
⊢ Complex.abs w ^ n / ↑r ^ n * (↑r⁻¹ * Complex.abs (f z)) = Complex.abs w ^ n * ↑(r⁻¹ ^ n) * (↑r⁻¹ * Complex.abs (f z))
Tactic:
rw [div_eq_mul_inv, ← inv_pow, NNReal.coe_pow, NNReal.coe_inv]
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
zs : Complex.abs (f z) ≤ ↑d
⊢ Complex.abs w ^ n * ↑(r⁻¹ ^ n) * (↑r⁻¹ * Complex.abs (f z)) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * (↑r⁻¹ * ↑d)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
hg : (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) = g
z : ℂ
zr : Complex.abs (z - c) = ↑r
zb : z ∈ closedBall c ↑r
zs : Complex.abs (f z) ≤ ↑d
⊢ Complex.abs w ^ n * ↑r⁻¹ ^ n * (↑r⁻¹ * ↑d) = Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d * ↑r⁻¹
Tactic:
ring
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
⊢ 0 ≤ π
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ |π|⁻¹ * 2⁻¹ * Complex.abs (circleIntegral g c ↑r) ≤ |π|⁻¹ * 2⁻¹ * (2 * π * ↑r * (wr * ↑r⁻¹))
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ |π|⁻¹ * 2⁻¹ * (2 * π * ↑r * (wr * ↑r⁻¹)) = π * |π|⁻¹ * (↑r * ↑r⁻¹) * wr
Tactic:
ring
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ π * |π|⁻¹ * (↑r * ↑r⁻¹) * wr = π * π⁻¹ * (↑r * ↑r⁻¹) * wr
Tactic:
rw [p3]
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ π * π⁻¹ * (↑r * ↑r⁻¹) * wr = 1 * (↑r * ↑r⁻¹) * wr
Tactic:
rw [mul_inv_cancel Real.pi_ne_zero]
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r d : ℝ≥0
w : ℂ
n : ℕ
rp : r > 0
h : ∀ w ∈ closedBall c ↑r, Complex.abs (f w) ≤ ↑d
wr : ℝ := Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
g : ℂ → ℂ
gs : ∀ z ∈ sphere c ↑r, ‖g z‖ ≤ wr * ↑r⁻¹
cn : Complex.abs (∮ (z : ℂ) in C(c, ↑r), g z) ≤ 2 * π * ↑r * (wr * ↑r⁻¹)
hg : (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) = g
p3 : |π| = π
⊢ 1 * (↑r * ↑r⁻¹) * wr = wr
Tactic:
rw [NNReal.coe_inv, mul_inv_cancel (NNReal.coe_ne_zero.mpr rp.ne'), one_mul, one_mul]
State after:
no goals