internlm/Lean-Github huggingface dataset:
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rw [← pp] at hp'
Proof state after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
refine hp'.hasSum ?_
Proof state after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ y ∈ EMetric.ball 0 ↑t.toNNReal
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ y ∈ EMetric.ball 0 ↑t.toNNReal
Tactic:
rw [EMetric.ball, Set.mem_setOf]
Proof state after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ edist y 0 < ↑t.toNNReal
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ edist y 0 < ↑t.toNNReal
Tactic:
calc edist y 0
  _ < t := t0
  _ = ↑t.toNNReal := (ENNReal.coe_toNNReal <| ne_top_of_lt t1).symm
Proof state after:
no goals
Theorem: analyticOn_ball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ t.toNNReal < r
Tactic:
rw [← WithTop.coe_lt_coe]
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ ↑t.toNNReal < ↑r
Theorem: analyticOn_ball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ ↑t.toNNReal < ↑r
Tactic:
exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof 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
Theorem: cauchy_bound
Proof 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]
Proof 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
Theorem: cauchy_bound
Proof 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
Proof 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
Theorem: cauchy_bound
Proof 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
Proof 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
Theorem: cauchy_bound
Proof 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
Proof 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
Theorem: cauchy_bound
Proof 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
Proof 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
Theorem: cauchy_bound
Proof 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 ⊢
Proof 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
Theorem: cauchy_bound
Proof 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)
Proof 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
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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]
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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₀]
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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]
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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
Proof 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⁻¹
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: cauchy_bound
Proof 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]
Proof state after:
no goals
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ circleIntegral f c r - circleIntegral g c r = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)) - circleIntegral g c r =
    circleIntegral (f - g) c r
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)) - circleIntegral g c r =
    circleIntegral (f - g) c r
Tactic:
generalize hf : (fun θ : ℝ ↦ deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - circleIntegral g c r = circleIntegral (f - g) c r