LeanPool.RiemannMappingTheorem.Spaces

@[reducible, inline]

abbrev 𝓒 (U : Set ℂ) : Type

𝓒 U : functions ℂ → ℂ equipped with the topology of locally uniform (compact-open) convergence on U.

Equations

• 𝓒 U = UniformOnFun ℂ ℂ (compacts U)

noncomputable def uderiv {U : Set ℂ} (f : 𝓒 U) : 𝓒 U

The complex derivative as a self-map on 𝓒 U.

Equations

• uderiv f = deriv f

theorem tendsto_𝓒_iff {U : Set ℂ} {ι : Type u_1} {l : Filter ι} (hU : IsOpen U) {F : ι → 𝓒 U} {f : 𝓒 U} : Filter.Tendsto F l (nhds f) ↔ TendstoLocallyUniformlyOn F f l U

def 𝓗 (U : Set ℂ) : Set (𝓒 U)

𝓗 U : the subspace of 𝓒 U consisting of holomorphic (complex-differentiable) functions on U.

Equations

• 𝓗 U = {f : 𝓒 U | DifferentiableOn ℂ f U}

theorem isClosed_𝓗 {U : Set ℂ} (hU : IsOpen U) : IsClosed (𝓗 U)

theorem ContinuousOn_uderiv {U : Set ℂ} (hU : IsOpen U) : ContinuousOn uderiv (𝓗 U)

def 𝓑 (U : Set ℂ) (Q : Set ℂ → Set ℂ) : Set (𝓒 U)

𝓑 U Q : the collection of holomorphic maps on U whose image on each compact K ⊆ U is contained in Q K. Used to formalise local boundedness conditions for normal-family arguments.

Equations

• 𝓑 U Q = {f : 𝓒 U | f ∈ 𝓗 U ∧ ∀ K ∈ compacts U, Set.MapsTo f K (Q K)}

theorem 𝓑_const {U Q : Set ℂ} : (𝓑 U fun (x : Set ℂ) => Q) = {f : 𝓒 U | f ∈ 𝓗 U ∧ Set.MapsTo f U Q}

theorem isClosed_𝓑 {U : Set ℂ} {Q : Set ℂ → Set ℂ} (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) : IsClosed (𝓑 U Q)

def 𝓜 (U : Set ℂ) : Set (𝓒 U)

𝓜 U : holomorphic functions on U whose image lies in the closed unit disk closedBall 0 1 ⊆ ℂ.

Equations

• 𝓜 U = {f : 𝓒 U | f ∈ 𝓗 U ∧ Set.MapsTo f U (Metric.closedBall 0 1)}

theorem 𝓜_eq_𝓑 {U : Set ℂ} : 𝓜 U = 𝓑 U fun (x : Set ℂ) => Metric.closedBall 0 1

theorem IsClosed_𝓜 {U : Set ℂ} (hU : IsOpen U) : IsClosed (𝓜 U)

def 𝓘 (U : Set ℂ) : Set (𝓒 U)

𝓘 U : holomorphic injections from U into the closed unit disk.

Equations

• 𝓘 U = {f : 𝓒 U | f ∈ 𝓜 U ∧ Set.InjOn f U}

theorem 𝓘_nonempty {U : Set ℂ} [good_domain U] : (𝓘 U).Nonempty

def 𝓙 (U : Set ℂ) : Set (𝓒 U)

𝓙 U : the closure of 𝓘 U in the compact-open topology — holomorphic maps U → closedBall 0 1 that are either injective or constant. Hurwitz's theorem says these are the only locally uniform limits of elements of 𝓘 U.

Equations

• 𝓙 U = {f : 𝓒 U | f ∈ 𝓜 U ∧ (Set.InjOn f U ∨ ∃ (w : ℂ), Set.EqOn f (fun (x : ℂ) => w) U)}

theorem 𝓘_subset_𝓙 {U : Set ℂ} : 𝓘 U ⊆ 𝓙 U