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

State before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
Tactic:
refine ContinuousOn.intervalIntegrable ?_
State after:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))

State before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul ?_ ?_
State after:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => w ^ n / (circleMap c (↑r) θ - c) ^ n) (Set.uIcc 0 (2 * π))

case refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹ * f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))

State before:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => w ^ n / (circleMap c (↑r) θ - c) ^ n) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul continuousOn_const ?_
State after:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹) (Set.uIcc 0 (2 * π))

State before:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹) (Set.uIcc 0 (2 * π))
Tactic:
apply Continuous.continuousOn
State after:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹

State before:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹
Tactic:
refine Continuous.inv₀ ?_ fun x ↦ pow_ne_zero n (circleMap_nz rp)
State after:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c) ^ n

State before:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c) ^ n
Tactic:
apply Continuous.pow
State after:
case refine_1.h.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun b => circleMap c (↑r) b - c

State before:
case refine_1.h.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun b => circleMap c (↑r) b - c
Tactic:
continuity
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹ * f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul ?_ ?_
State after:
case refine_2.refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹) (Set.uIcc 0 (2 * π))

case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))

State before:
case refine_2.refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹) (Set.uIcc 0 (2 * π))
Tactic:
apply Continuous.continuousOn
State after:
case refine_2.refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c)⁻¹

State before:
case refine_2.refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c)⁻¹
Tactic:
refine Continuous.inv₀ (by continuity) fun x ↦ circleMap_nz rp
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => circleMap c (↑r) θ - c
Tactic:
continuity
State after:
no goals

State before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.comp h (Continuous.continuousOn (by continuity)) ?_
State after:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Set.MapsTo (fun θ => circleMap c (↑r) θ) (Set.uIcc 0 (2 * π)) (closedBall c ↑r)

State before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Set.MapsTo (fun θ => circleMap c (↑r) θ) (Set.uIcc 0 (2 * π)) (closedBall c ↑r)
Tactic:
intro θ _
State after:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
θ : ℝ
a✝ : θ ∈ Set.uIcc 0 (2 * π)
⊢ (fun θ => circleMap c (↑r) θ) θ ∈ closedBall c ↑r

State before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
θ : ℝ
a✝ : θ ∈ Set.uIcc 0 (2 * π)
⊢ (fun θ => circleMap c (↑r) θ) θ ∈ closedBall c ↑r
Tactic:
exact circleMap_mem_closedBall c (NNReal.coe_nonneg r) θ
State after:
no goals

State before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => circleMap c (↑r) θ
Tactic:
continuity
State after:
no goals