[GOAL]
α : Type ?u.37
β : Type ?u.40
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
⊢ inst✝¹ ≤ OuterMeasure.caratheodory (OuterMeasure.dirac a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
⊢ ↑↑(dirac a) s = 1
[PROOFSTEP]
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s = 1
[PROOFSTEP]
refine' le_antisymm (this univ trivial ▸ _) (this s h ▸ le_dirac_apply)
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ indicator univ 1 a
[PROOFSTEP]
rw [← dirac_apply' a MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type ?u.2205
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ ↑↑(dirac a) univ
[PROOFSTEP]
exact measure_mono (subset_univ s)
[GOAL]
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
[GOAL]
case neg
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
[PROOFSTEP]
rw [indicator_of_not_mem h, ← nonpos_iff_eq_zero]
[GOAL]
case neg
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s ≤ 0
[PROOFSTEP]
calc
  dirac a s ≤ dirac a { a }ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
  _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
[GOAL]
α : Type u_1
β : Type ?u.3101
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) {a}ᶜ = 0
[PROOFSTEP]
simp [dirac_apply' _ (measurableSet_singleton _).compl]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f (dirac a)) s = ↑↑(dirac (f a)) s
[PROOFSTEP]
simp [hs, map_apply hf hs, hf hs, indicator_apply]
[GOAL]
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
a : α
⊢ restrict μ {a} = ↑↑μ {a} • dirac a
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
have : s ∩ { a } = { a } := by simpa
[GOAL]
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}
[PROOFSTEP]
simpa
[GOAL]
case pos
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
have : s ∩ { a } = ∅ := inter_singleton_eq_empty.2 ha
[GOAL]
case neg
α : Type u_1
β : Type ?u.7321
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
this : s ∩ {a} = ∅
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
[PROOFSTEP]
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' { y }) := fun y _ => hf (measurableSet_singleton _)
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
this : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
[PROOFSTEP]
simp [← tsum_measure_preimage_singleton (to_countable s) this, *, tsum_subtype s fun b => μ (f ⁻¹' { b }), ←
  indicator_mul_right s fun b => μ (f ⁻¹' { b })]
[GOAL]
α : Type u_1
β : Type ?u.17308
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun a => ↑↑μ {a} • dirac a) = μ
[PROOFSTEP]
simpa using (map_eq_sum μ id measurable_id).symm
[GOAL]
α : Type u_1
β : Type ?u.19567
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), indicator s (fun x => ↑↑μ {x}) x = ↑↑(sum fun a => ↑↑μ {a} • dirac a) s
[PROOFSTEP]
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, Set.indicator_apply, mul_ite,
  Pi.one_apply, mul_one, mul_zero]
[GOAL]
α : Type u_1
β : Type ?u.19567
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum fun a => ↑↑μ {a} • dirac a) s = ↑↑μ s
[PROOFSTEP]
rw [μ.sum_smul_dirac]
[GOAL]
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
h : a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]
[GOAL]
case neg
α : Type u_1
β : Type ?u.22509
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
h : ¬a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
[PROOFSTEP]
simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]
[GOAL]
α : Type u_1
β : Type ?u.24298
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type ?u.24298
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a
[PROOFSTEP]
simp [mem_ae_iff, imp_false]
[GOAL]
α : Type u_2
β : Type ?u.26464
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
δ : Type u_1
inst✝ : MeasurableSingletonClass α
a : α
f : α → δ
⊢ f =ᶠ[ae (dirac a)] const α (f a)
[PROOFSTEP]
simp [Filter.EventuallyEq]
[GOAL]
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ Measure.restrict (dirac a) s = if a ∈ s then dirac a else 0
[PROOFSTEP]
split_ifs with has
[GOAL]
case pos
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ Measure.restrict (dirac a) s = dirac a
[PROOFSTEP]
apply restrict_eq_self_of_ae_mem
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
[PROOFSTEP]
rw [ae_dirac_iff]
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ a ∈ s
[PROOFSTEP]
assumption
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ MeasurableSet {x | x ∈ s}
[PROOFSTEP]
assumption
[GOAL]
case neg
α : Type u_1
β : Type ?u.27478
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : ¬a ∈ s
⊢ Measure.restrict (dirac a) s = 0
[PROOFSTEP]
rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_not_mem has]
[GOAL]
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ Measure.restrict (dirac a) s = if a ∈ s then dirac a else 0
[PROOFSTEP]
split_ifs with has
[GOAL]
case pos
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ Measure.restrict (dirac a) s = dirac a
[PROOFSTEP]
apply restrict_eq_self_of_ae_mem
[GOAL]
case pos.hs
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
[PROOFSTEP]
rwa [ae_dirac_eq]
[GOAL]
case neg
α : Type u_1
β : Type ?u.28375
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : ¬a ∈ s
⊢ Measure.restrict (dirac a) s = 0
[PROOFSTEP]
rw [restrict_eq_zero, dirac_apply, indicator_of_not_mem has]


[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