[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
[PROOFSTEP]
have := periodic_circleMap
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)
⊢ Periodic (circleTransformDeriv R z w f) (2 * π)
[PROOFSTEP]
simp_rw [Periodic] at *
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
⊢ ∀ (x : ℝ), circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
[PROOFSTEP]
intro x
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x
[PROOFSTEP]
simp_rw [circleTransformDeriv, this]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ (2 * ↑π * I)⁻¹ • deriv (circleMap z R) (x + 2 * π) • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x) =
    (2 * ↑π * I)⁻¹ • deriv (circleMap z R) x • ((circleMap z R x - w) ^ 2)⁻¹ • f (circleMap z R x)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x
[PROOFSTEP]
simp [this]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ circleTransformDeriv R z w f = fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
[PROOFSTEP]
ext
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ circleTransformDeriv R z w f x✝ = (circleMap z R x✝ - w)⁻¹ • circleTransform R z w f x✝
[PROOFSTEP]
simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹) • f (circleMap z R x✝) =
    ((circleMap z R x✝ - w)⁻¹ * (2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹) •
      f (circleMap z R x✝)
[PROOFSTEP]
ring_nf
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹ ^ 2 * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
[PROOFSTEP]
rw [inv_pow]
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ *
        (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝) =
    ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹ * (↑(Int.ofNat 1) / ↑2)) •
      f (circleMap z R x✝)
[PROOFSTEP]
congr
[GOAL]
case h.e_a.e_a.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ -(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2 = (circleMap z R x✝ - w) ^ 2
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0 ..2 * π, circleTransform R z w f θ = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
[PROOFSTEP]
simp_rw [circleTransform, circleIntegral, deriv_circleMap, circleMap]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0 ..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I)) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0 ..2 * π, ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I))
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransform R z w f)
[PROOFSTEP]
apply_rules [Continuous.smul, continuous_const]
[GOAL]
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => deriv (circleMap z R) x
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => (circleMap z R x - w)⁻¹
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => f (circleMap z R x)
[PROOFSTEP]
simp_rw [deriv_circleMap]
[GOAL]
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => circleMap 0 R x * I
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => (circleMap z R x - w)⁻¹
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => f (circleMap z R x)
[PROOFSTEP]
apply_rules [Continuous.mul, continuous_circleMap 0 R, continuous_const]
[GOAL]
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => (circleMap z R x - w)⁻¹
[PROOFSTEP]
apply continuous_circleMap_inv hw
[GOAL]
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => f (circleMap z R x)
[PROOFSTEP]
apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)
[GOAL]
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R
[PROOFSTEP]
exact fun _ => (circleMap_mem_sphere _ hR.le) _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransformDeriv R z w f)
[PROOFSTEP]
rw [circleTransformDeriv_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w✝ : ℂ
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
[PROOFSTEP]
exact (continuous_circleMap_inv hw).smul (continuous_circleTransform hR hf hw)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (circleMap z R w.snd - w.fst)⁻¹ ^ 2) (closedBall z r ×ˢ univ)
[PROOFSTEP]
simp_rw [← one_div]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (1 / (circleMap z R w.snd - w.fst)) ^ 2) (closedBall z r ×ˢ univ)
[PROOFSTEP]
apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
[GOAL]
case hf.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap z R x.snd - x.fst) (closedBall z r ×ˢ univ)
case hf.h₀
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
[PROOFSTEP]
refine'
  ((continuous_circleMap z R).continuousOn.comp continuousOn_snd fun _ => And.right).sub
    (continuousOn_id.comp continuousOn_fst fun _ => And.left)
[GOAL]
case hf.h₀
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
[PROOFSTEP]
simp only [mem_prod, Ne.def, and_imp, Prod.forall]
[GOAL]
case hf.h₀
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (a : ℂ) (b : ℝ), a ∈ closedBall z r → b ∈ univ → ¬circleMap z R b - a = 0
[PROOFSTEP]
intro a b ha _
[GOAL]
case hf.h₀
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
⊢ ¬circleMap z R b - a = 0
[PROOFSTEP]
have ha2 : a ∈ ball z R := by simp at *; linarith
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
⊢ a ∈ ball z R
[PROOFSTEP]
simp at *
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : dist a z ≤ r
a✝ : True
⊢ dist a z < R
[PROOFSTEP]
linarith
[GOAL]
case hf.h₀
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
ha2 : a ∈ ball z R
⊢ ¬circleMap z R b - a = 0
[PROOFSTEP]
exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
[PROOFSTEP]
have : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ (⊤ : Set ℝ)) :=
  by
  apply_rules [ContinuousOn.smul, continuousOn_const]
  simp only [deriv_circleMap]
  have c := (continuous_circleMap 0 R).continuousOn (s := ⊤)
  apply_rules [ContinuousOn.mul, c.comp continuousOn_snd fun _ => And.right, continuousOn_const]
  simp_rw [← inv_pow]
  apply continuousOn_prod_circle_transform_function hr
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
apply_rules [ContinuousOn.smul, continuousOn_const]
[GOAL]
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => deriv (circleMap z R) x.snd) (closedBall z r ×ˢ ⊤)
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.snd - x.fst) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
simp only [deriv_circleMap]
[GOAL]
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.snd - x.fst) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
have c := (continuous_circleMap 0 R).continuousOn (s := ⊤)
[GOAL]
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
c : ContinuousOn (circleMap 0 R) ⊤
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.snd - x.fst) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
apply_rules [ContinuousOn.mul, c.comp continuousOn_snd fun _ => And.right, continuousOn_const]
[GOAL]
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.snd - x.fst) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
simp_rw [← inv_pow]
[GOAL]
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => (circleMap z R x.snd - x.fst)⁻¹ ^ 2) (closedBall z r ×ˢ ⊤)
[PROOFSTEP]
apply continuousOn_prod_circle_transform_function hr
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
[PROOFSTEP]
refine' continuous_abs.continuousOn (s := ⊤).comp this _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
[PROOFSTEP]
show MapsTo _ _ (⊤ : Set ℂ)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
[PROOFSTEP]
simp [MapsTo]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
have cts := continuousOn_abs_circleTransformBoundingFunction hr z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
  apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
⊢ IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
[PROOFSTEP]
apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty := (nonempty_closedBall.2 hr').prod nonempty_uIcc
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
have :=
  IsCompact.exists_isMaxOn comp none
    (cts.mono (by intro z; simp only [mem_prod, mem_closedBall, mem_univ, and_true_iff, and_imp]; tauto))
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z r ×ˢ [[0, 2 * π]])
⊢ closedBall z r ×ˢ [[0, 2 * π]] ⊆ closedBall z r ×ˢ univ
[PROOFSTEP]
intro z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝¹ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z✝ : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z✝ t) (closedBall z✝ r ×ˢ univ)
comp : IsCompact (closedBall z✝ r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z✝ r ×ˢ [[0, 2 * π]])
z : ℂ × ℝ
⊢ z ∈ closedBall z✝ r ×ˢ [[0, 2 * π]] → z ∈ closedBall z✝ r ×ˢ univ
[PROOFSTEP]
simp only [mem_prod, mem_closedBall, mem_univ, and_true_iff, and_imp]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝¹ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z✝ : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z✝ t) (closedBall z✝ r ×ˢ univ)
comp : IsCompact (closedBall z✝ r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z✝ r ×ˢ [[0, 2 * π]])
z : ℂ × ℝ
⊢ dist z.fst z✝ ≤ r → z.snd ∈ [[0, 2 * π]] → dist z.fst z✝ ≤ r
[PROOFSTEP]
tauto
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z r ×ˢ [[0, 2 * π]])
this :
  ∃ x,
    x ∈ closedBall z r ×ˢ [[0, 2 * π]] ∧
      IsMaxOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
simp only [IsMaxOn, IsMaxFilter] at this 
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : Set.Nonempty (closedBall z r ×ˢ [[0, 2 * π]])
this :
  ∃ x,
    x ∈ closedBall z r ×ˢ [[0, 2 * π]] ∧
      ∀ᶠ (x_1 : ℂ × ℝ) in 𝓟 (closedBall z r ×ˢ [[0, 2 * π]]),
        (↑abs ∘ fun t => circleTransformBoundingFunction R z t) x_1 ≤
          (↑abs ∘ fun t => circleTransformBoundingFunction R z t) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ↑abs (circleTransformBoundingFunction R z ↑y) ≤ ↑abs (circleTransformBoundingFunction R z ↑x)
[PROOFSTEP]
simpa [SetCoe.forall, Subtype.coe_mk, SetCoe.exists]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
obtain ⟨r, hr, hrx⟩ := exists_lt_mem_ball_of_mem_ball hx
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
obtain ⟨ε', hε', H⟩ := exists_ball_subset_ball hrx
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
obtain ⟨⟨⟨a, b⟩, ⟨ha, hb⟩⟩, hab⟩ := abs_circleTransformBoundingFunction_le hr (pos_of_mem_ball hrx).le z
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
let V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun _ => 1) θ
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
have funccomp : ContinuousOn (fun r => abs (f r)) (sphere z R) :=
  by
  have cabs : ContinuousOn abs ⊤ := by apply continuous_abs.continuousOn
  apply cabs.comp hf; rw [MapsTo]; tauto
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
⊢ ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
[PROOFSTEP]
have cabs : ContinuousOn abs ⊤ := by apply continuous_abs.continuousOn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
⊢ ContinuousOn ↑abs ⊤
[PROOFSTEP]
apply continuous_abs.continuousOn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
cabs : ContinuousOn ↑abs ⊤
⊢ ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
[PROOFSTEP]
apply cabs.comp hf
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
cabs : ContinuousOn ↑abs ⊤
⊢ MapsTo f (sphere z R) ⊤
[PROOFSTEP]
rw [MapsTo]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
cabs : ContinuousOn ↑abs ⊤
⊢ ∀ ⦃x : ℂ⦄, x ∈ sphere z R → f x ∈ ⊤
[PROOFSTEP]
tauto
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
have sbou := IsCompact.exists_isMaxOn (isCompact_sphere z R) (NormedSpace.sphere_nonempty.2 hR.le) funccomp
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
sbou : ∃ x, x ∈ sphere z R ∧ IsMaxOn (fun r => ↑abs (f r)) (sphere z R) x
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
obtain ⟨X, HX, HX2⟩ := sbou
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε → ‖circleTransformDeriv R z y f t‖ ≤ B
[PROOFSTEP]
refine' ⟨abs (V b a) * abs (f X), ε', hε', Subset.trans H (ball_subset_ball hr.le), _⟩
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
⊢ ∀ (t : ℝ) (y : ℂ), y ∈ ball x ε' → ‖circleTransformDeriv R z y f t‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
intro y v hv
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
obtain ⟨y1, hy1, hfun⟩ := Periodic.exists_mem_Ico₀ (circleTransformDeriv_periodic R z v f) Real.two_pi_pos y
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
have hy2 : y1 ∈ [[0, 2 * π]] := by
  convert Ico_subset_Icc_self hy1 using 1
  simp [uIcc_of_le Real.two_pi_pos.le]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
⊢ y1 ∈ [[0, 2 * π]]
[PROOFSTEP]
convert Ico_subset_Icc_self hy1 using 1
[GOAL]
case h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
⊢ [[0, 2 * π]] = Icc 0 (2 * π)
[PROOFSTEP]
simp [uIcc_of_le Real.two_pi_pos.le]
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
HX2 : IsMaxOn (fun r => ↑abs (f r)) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
simp only [IsMaxOn, IsMaxFilter, eventually_principal, mem_sphere_iff_norm, norm_eq_abs] at HX2 
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ↑abs (x - z) = R → ↑abs (f x) ≤ ↑abs (f X)
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
have :=
  mul_le_mul (hab ⟨⟨v, y1⟩, ⟨ball_subset_closedBall (H hv), hy2⟩⟩)
    (HX2 (circleMap z R y1) (circleMap_mem_sphere z hR.le y1)) (Complex.abs.nonneg _) (Complex.abs.nonneg _)
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ↑abs (x - z) = R → ↑abs (f x) ≤ ↑abs (f X)
this :
  ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (v, y1), property := (_ : (v, y1).fst ∈ closedBall z r ∧ (v, y1).snd ∈ [[0, 2 * π]]) }) *
      ↑abs (f (circleMap z R y1)) ≤
    ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) }) *
      ↑abs (f X)
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ↑abs (V b a) * ↑abs (f X)
[PROOFSTEP]
simp_rw [hfun]
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ↑abs (circleTransformBoundingFunction R z ↑y) ≤
      ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) })
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
HX : X ∈ sphere z R
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ↑abs (x - z) = R → ↑abs (f x) ≤ ↑abs (f X)
this :
  ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (v, y1), property := (_ : (v, y1).fst ∈ closedBall z r ∧ (v, y1).snd ∈ [[0, 2 * π]]) }) *
      ↑abs (f (circleMap z R y1)) ≤
    ↑abs
        (circleTransformBoundingFunction R z
          ↑{ val := (a, b), property := (_ : (a, b).fst ∈ closedBall z r ∧ (a, b).snd ∈ [[0, 2 * π]]) }) *
      ↑abs (f X)
⊢ ‖circleTransformDeriv R z v f y1‖ ≤ ↑abs (circleTransformDeriv R z a (fun x => 1) b) * ↑abs (f X)
[PROOFSTEP]
simp only [circleTransformBoundingFunction, circleTransformDeriv, norm_eq_abs, Algebra.id.smul_eq_mul, deriv_circleMap,
  map_mul, abs_circleMap_zero, abs_I, mul_one, ← mul_assoc, mul_inv_rev, inv_I, abs_neg, abs_inv, abs_ofReal, one_mul,
  abs_two, abs_pow, mem_ball, gt_iff_lt, Subtype.coe_mk, SetCoe.forall, mem_prod, mem_closedBall, and_imp, Prod.forall,
  NormedSpace.sphere_nonempty, mem_sphere_iff_norm] at *
[GOAL]
case intro.intro.intro.intro.intro.mk.mk.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
ε' : ℝ
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).fst ∈ closedBall z r
hb : (a, b).snd ∈ [[0, 2 * π]]
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
funccomp : ContinuousOn (fun r => ↑abs (f r)) (sphere z R)
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ↑abs (x - z) = R → ↑abs (f x) ≤ ↑abs (f X)
hx : dist x z < R
hrx : dist x z < r
hε' : 0 < ε'
hab :
  ∀ (a_1 : ℂ) (b_1 : ℝ),
    dist a_1 z ≤ r →
      b_1 ∈ [[0, 2 * π]] →
        ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R b_1 - a_1) ^ 2)⁻¹ ≤
          ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R b - a) ^ 2)⁻¹
HX : ↑abs (X - z) = R
hfun :
  -I * (↑π)⁻¹ * 2⁻¹ * circleMap 0 R y * I * ((circleMap z R y - v) ^ 2)⁻¹ * f (circleMap z R y) =
    -I * (↑π)⁻¹ * 2⁻¹ * circleMap 0 R y1 * I * ((circleMap z R y1 - v) ^ 2)⁻¹ * f (circleMap z R y1)
this :
  ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R y1 - v) ^ 2)⁻¹ * ↑abs (f (circleMap z R y1)) ≤
    ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R b - a) ^ 2)⁻¹ * ↑abs (f X)
⊢ ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R y1 - v) ^ 2)⁻¹ * ↑abs (f (circleMap z R y1)) ≤
    ↑abs (-I) * ↑abs (↑π)⁻¹ * ↑abs 2⁻¹ * |R| * ↑abs ((circleMap z R b - a) ^ 2)⁻¹ * ↑abs (f X)
[PROOFSTEP]
exact this
