[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
[PROOFSTEP]
have minor₁ : ‖map 1‖ ≠ 0 := by simpa only [ext_ring_iff, Ne.def, norm_eq_zero] using nonzero
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ ‖↑map 1‖ ≠ 0
[PROOFSTEP]
simpa only [ext_ring_iff, Ne.def, norm_eq_zero] using nonzero
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
[PROOFSTEP]
refine' ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), _⟩, _⟩
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
[PROOFSTEP]
simp only [LinearMap.smul_apply]
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
[PROOFSTEP]
have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ x = x • 1
[PROOFSTEP]
rw [smul_eq_mul, mul_one]
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
[PROOFSTEP]
nth_rw 1 [this]
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) (x • 1)‖ = ‖x‖
[PROOFSTEP]
rw [LinearMap.coe_restrictScalars]
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑↑map (x • 1)‖ = ‖x‖
[PROOFSTEP]
simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖↑map 1‖⁻¹ * (‖x‖ * ‖↑map 1‖) = ‖x‖
[PROOFSTEP]
field_simp only [one_mul]
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ restrictScalars ℝ map =
    ‖↑map 1‖ •
      LinearIsometry.toContinuousLinearMap
        { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := (_ : ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖) }
[PROOFSTEP]
ext1
  -- Porting note: was simp
[GOAL]
case refine'_2.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x✝ : ℂ
⊢ ↑(restrictScalars ℝ map) x✝ =
    ↑(‖↑map 1‖ •
          LinearIsometry.toContinuousLinearMap
            { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := (_ : ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖) })
      x✝
[PROOFSTEP]
rw [coe_restrictScalars', coe_smul', LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.coe_mk, Pi.smul_apply,
  LinearMap.smul_apply, LinearMap.coe_restrictScalars, coe_coe, smul_inv_smul₀ minor₁]
[GOAL]
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h : IsConformalMap g
⊢ (∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = ContinuousLinearMap.comp g ↑conjCle
[PROOFSTEP]
rcases h with ⟨c, -, li, rfl⟩
[GOAL]
case intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap li) ∨
    ∃ map, restrictScalars ℝ map = ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap li) ↑conjCle
[PROOFSTEP]
obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li := ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩
[GOAL]
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ LinearIsometryEquiv.toLinearIsometry
      (LinearIsometry.toLinearIsometryEquiv li (_ : FiniteDimensional.finrank ℝ ℂ = FiniteDimensional.finrank ℝ ℂ)) =
    li
[PROOFSTEP]
ext1
[GOAL]
case h
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.toLinearIsometry
          (LinearIsometry.toLinearIsometryEquiv li (_ : FiniteDimensional.finrank ℝ ℂ = FiniteDimensional.finrank ℝ ℂ)))
      x✝ =
    ↑li x✝
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li)) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li))
          ↑conjCle
[PROOFSTEP]
rcases linear_isometry_complex li with
  ⟨a, rfl | rfl⟩
    -- let rot := c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ,
[GOAL]
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ↑conjCle
[PROOFSTEP]
refine' Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
[GOAL]
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))
[PROOFSTEP]
ext1
  -- Porting note: was simp
[GOAL]
case intro.intro.intro.intro.intro.inl.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) x✝
[PROOFSTEP]
rw [coe_restrictScalars', smul_apply, smul_apply, smul_apply, LinearIsometry.coe_toContinuousLinearMap,
  LinearIsometryEquiv.coe_toLinearIsometry, rotation_apply, id_apply, smul_eq_mul]
[GOAL]
case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c •
          LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a)))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle
[PROOFSTEP]
refine' Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
[GOAL]
case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    ContinuousLinearMap.comp
      (c •
        LinearIsometry.toContinuousLinearMap
          (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
      ↑conjCle
[PROOFSTEP]
ext1
  -- Porting note: was simp
[GOAL]
case intro.intro.intro.intro.intro.inr.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle)
      x✝
[PROOFSTEP]
rw [coe_restrictScalars', smul_apply, smul_apply, comp_apply, smul_apply, LinearIsometry.coe_toContinuousLinearMap,
  LinearIsometryEquiv.coe_toLinearIsometry, LinearIsometryEquiv.trans_apply, rotation_apply, id_apply, smul_eq_mul,
  ContinuousLinearEquiv.coe_coe, conjCle_apply, conjLie_apply, conj_conj]
[GOAL]
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g ↔ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0
[PROOFSTEP]
exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩
[GOAL]
case mpr
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0 → IsConformalMap g
[PROOFSTEP]
rintro ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩
[GOAL]
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
[PROOFSTEP]
refine' isConformalMap_complex_linear _
[GOAL]
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ map ≠ 0
[PROOFSTEP]
contrapose! h₂ with w
[GOAL]
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ restrictScalars ℝ map = 0
[PROOFSTEP]
simp only [w, restrictScalars_zero]
[GOAL]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
⊢ IsConformalMap g
[PROOFSTEP]
have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCle := by
  ext1
  simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply, conjCle_apply, starRingEnd_self_apply]
[GOAL]
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
⊢ g = comp (restrictScalars ℝ map) ↑conjCle
[PROOFSTEP]
ext1
[GOAL]
case h
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
x✝ : ℂ
⊢ ↑g x✝ = ↑(comp (restrictScalars ℝ map) ↑conjCle) x✝
[PROOFSTEP]
simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply, conjCle_apply, starRingEnd_self_apply]
[GOAL]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap g
[PROOFSTEP]
rw [minor₁] at h₂ ⊢
[GOAL]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap (comp (restrictScalars ℝ map) ↑conjCle)
[PROOFSTEP]
refine' isConformalMap_complex_linear_conj _
[GOAL]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ map ≠ 0
[PROOFSTEP]
contrapose! h₂ with w
[GOAL]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
w : map = 0
⊢ comp (restrictScalars ℝ map) ↑conjCle = 0
[PROOFSTEP]
simp only [w, restrictScalars_zero, zero_comp]


[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
R : ℝ
c : ℂ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
⊢ deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-2) • f z
[PROOFSTEP]
lift R to ℝ≥0 using hR.le
[GOAL]
case intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z
[PROOFSTEP]
refine' (hf.hasFPowerSeriesOnBall hR).hasFPowerSeriesAt.deriv.trans _
[GOAL]
case intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ (↑(cauchyPowerSeries f c (↑R) 1) fun x => 1) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z
[PROOFSTEP]
simp only [cauchyPowerSeries_apply, one_div, zpow_neg, pow_one, smul_smul, zpow_two, mul_inv]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R
[PROOFSTEP]
have : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2 : ℤ) • f z‖ ≤ C / (R * R) := fun z (hz : abs (z - c) = R) => by
  simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using (div_le_div_right (mul_pos hR hR)).2 (hC z hz)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
z : ℂ
hz : ↑abs (z - c) = R
⊢ ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
[PROOFSTEP]
simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using (div_le_div_right (mul_pos hR hR)).2 (hC z hz)
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ∀ (z : ℂ), z ∈ sphere c R → ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ ‖deriv f c‖ ≤ C / R
[PROOFSTEP]
calc
  ‖deriv f c‖ = ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z‖ :=
    congr_arg norm (deriv_eq_smul_circleIntegral hR hf)
  _ ≤ R * (C / (R * R)) := (circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le this)
  _ = C / R := by rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]
[GOAL]
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
this : ∀ (z : ℂ), z ∈ sphere c R → ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ R * (C / (R * R)) = C / R
[PROOFSTEP]
rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R
[PROOFSTEP]
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R
[PROOFSTEP]
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
  e.hasFDerivAt.comp_hasDerivAt c (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R
[PROOFSTEP]
calc
  ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
    rw [this.deriv]
    exact (UniformSpace.Completion.norm_coe _).symm
  _ ≤ C / R :=
    norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
      (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖deriv (↑e ∘ f) c‖
[PROOFSTEP]
rw [this.deriv]
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖↑e (deriv f c)‖
[PROOFSTEP]
exact (UniformSpace.Completion.norm_coe _).symm
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ f z = f w
[PROOFSTEP]
suffices : ∀ c, deriv f c = 0
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
this : ∀ (c : ℂ), deriv f c = 0
⊢ f z = f w
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
[PROOFSTEP]
exact is_const_of_deriv_eq_zero hf this z w
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : ℂ
⊢ ∀ (c : ℂ), deriv f c = 0
[PROOFSTEP]
clear z w
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
⊢ ∀ (c : ℂ), deriv f c = 0
[PROOFSTEP]
intro c
[GOAL]
case this
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
⊢ deriv f c = 0
[PROOFSTEP]
obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C :=
  by
  rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
  exact ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z => (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
⊢ ∃ C, C > 0 ∧ ∀ (z : ℂ), ‖f z‖ ≤ C
[PROOFSTEP]
rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
[GOAL]
case intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
hC : ∀ (x : F), x ∈ range f → ‖x‖ ≤ C
⊢ ∃ C, C > 0 ∧ ∀ (z : ℂ), ‖f z‖ ≤ C
[PROOFSTEP]
exact ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z => (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
[GOAL]
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0
[PROOFSTEP]
refine' norm_le_zero_iff.1 (le_of_forall_le_of_dense fun ε ε₀ => _)
[GOAL]
case this.intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε
[PROOFSTEP]
calc
  ‖deriv f c‖ ≤ C / (C / ε) :=
    norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.diffContOnCl fun z _ => hC z
  _ = ε := div_div_cancel' C₀.lt.ne'
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
⊢ f z = f w
[PROOFSTEP]
set g : ℂ → F := f ∘ fun t : ℂ => t • (w - z) + z
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ f z = f w
[PROOFSTEP]
suffices g 0 = g 1 by simpa
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
this : g 0 = g 1
⊢ f z = f w
[PROOFSTEP]
simpa
[GOAL]
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ g 0 = g 1
[PROOFSTEP]
apply liouville_theorem_aux
[GOAL]
case hf
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Differentiable ℂ g
case hb
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Metric.Bounded (range g)
[PROOFSTEP]
exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z), hb.mono (range_comp_subset_range _ _)]


[GOAL]
⊢ CommSemigroup 𝔻
[PROOFSTEP]
unfold UnitDisc
[GOAL]
⊢ CommSemigroup ↑(ball 0 1)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasDistribNeg 𝔻
[PROOFSTEP]
unfold UnitDisc
[GOAL]
⊢ HasDistribNeg ↑(ball 0 1)
[PROOFSTEP]
infer_instance
[GOAL]
z : 𝔻
⊢ ↑normSq ↑z < 1
[PROOFSTEP]
convert (Real.sqrt_lt' one_pos).1 z.abs_lt_one
[GOAL]
case h.e'_4
z : 𝔻
⊢ 1 = 1 ^ 2
[PROOFSTEP]
exact (one_pow 2).symm
[GOAL]
z : 𝔻
⊢ ↑abs ↑z ≠ ↑abs (-1)
[PROOFSTEP]
rw [abs.map_neg, map_one]
[GOAL]
z : 𝔻
⊢ ↑abs ↑z ≠ 1
[PROOFSTEP]
exact z.abs_ne_one