LeanPool.RiemannMappingTheorem.Defs

def compacts (U : Set ℂ) : Set (Set ℂ)

The collection of compact subsets of U. Used as the index for the compact-open topology 𝓒 U.

Equations

• compacts U = {K : Set ℂ | K ⊆ U ∧ IsCompact K}

@[simp]

theorem union_compacts {U : Set ℂ} : ⋃₀ compacts U = U

def 𝔻 : Set ℂ

The open unit disk {z : ℂ | ‖z‖ < 1}.

Equations

• 𝔻 = Metric.ball 0 1

theorem mem_𝔻_iff {u : ℂ} : u ∈ 𝔻 ↔ ‖u‖ < 1

theorem neg_in_𝔻 {u : ℂ} : u ∈ 𝔻 → -u ∈ 𝔻

theorem sqrt_𝔻_eq_𝔻 : {z : ℂ | z ^ 2 ∈ 𝔻} = 𝔻

class good_domain (U : Set ℂ) : Prop

A good_domain is a connected proper open nonempty subset of ℂ on which every nowhere-zero holomorphic function admits a holomorphic square root. The variant of the Riemann Mapping Theorem proved here applies to such domains.

• is_open : IsOpen U

  U is open.

• is_nonempty : U.Nonempty

  U is nonempty.

• is_preconnected : IsPreconnected U

  U is preconnected.

• ne_univ : U ≠ Set.univ

  U is a proper subset of ℂ.

• hasSqrt (f : ℂ → ℂ) : (∀ z ∈ U, f z ≠ 0) → DifferentiableOn ℂ f U → ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g U ∧ Set.EqOn f (g ^ 2) U

  Every nowhere-zero holomorphic function on U has a holomorphic square root.

structure embedding (U V : Set ℂ) : Type

An embedding U V is a holomorphic injection ℂ → ℂ whose restriction to U lands in V. Used to package the various conformal maps that build the Riemann-mapping isomorphism.

• toFun : ℂ → ℂ

  The underlying function ℂ → ℂ.

• is_diff : DifferentiableOn ℂ self.toFun U

  The function is holomorphic on U.

• is_inj : Set.InjOn self.toFun U

  The function is injective on U.

• maps_to : Set.MapsTo self.toFun U V

  The function maps U into V.

@[implicit_reducible]

instance instCoeFunEmbeddingForallComplex {U V : Set ℂ} : CoeFun (embedding U V) fun (x : embedding U V) => ℂ → ℂ

Equations

• instCoeFunEmbeddingForallComplex = { coe := embedding.toFun }

def embedding.id {U V : Set ℂ} (hUV : U = V) : embedding U V

The identity embedding U → U, lifted to an embedding U V whenever U = V.

Equations

• embedding.id hUV = { toFun := fun (x : ℂ) => x, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }

def embedding.comp {U V W : Set ℂ} (f : embedding V W) (g : embedding U V) : embedding U W

Composition of embeddings: (f ∘ g) : embedding U W.

Equations

• f.comp g = { toFun := f.toFun ∘ g.toFun, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }

noncomputable def embedding.sqrt {U V : Set ℂ} [good_domain U] (f : embedding U V) (hf : ∀ z ∈ U, f.toFun z ≠ 0) : { g : embedding U {z : ℂ | z ^ 2 ∈ V} // Set.EqOn f.toFun (g.toFun ^ 2) U }

Lift a nowhere-zero embedding U → V to an embedding U → {z | z² ∈ V} by taking a holomorphic square root supplied by good_domain.hasSqrt.

Equations

• f.sqrt hf = (fun (g : ℂ → ℂ) (x : DifferentiableOn ℂ g U ∧ Set.EqOn f.toFun (g ^ 2) U) => ⟨{ toFun := g, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }, ⋯⟩) (Classical.choose ⋯) ⋯

noncomputable def embedding.sqrt' {U : Set ℂ} [good_domain U] (f : embedding U 𝔻) (hf : ∀ z ∈ U, f.toFun z ≠ 0) : { g : embedding U 𝔻 // Set.EqOn f.toFun (g.toFun ^ 2) U }

Specialisation of embedding.sqrt when the codomain is the open unit disk 𝔻: the square root again lands in 𝔻.

Equations

• f.sqrt' hf = match f.sqrt hf with | ⟨g, hg⟩ => ⟨(embedding.id sqrt_𝔻_eq_𝔻).comp g, hg⟩

theorem ne_center_of_not_mem_closed_ball {w : ℂ} {r : ℝ} (hr : 0 ≤ r) ⦃z : ℂ⦄ (hz : z ∈ (Metric.closedBall w r)ᶜ) : z ≠ w

noncomputable def embedding.inv (w : ℂ) {r : ℝ} (hr : 0 < r) : embedding (Metric.closedBall w r)ᶜ 𝔻

The conformal inversion z ↦ r / (z - w) realised as an embedding from the complement of the closed disk closedBall w r into the open unit disk.

Equations

• embedding.inv w hr = { toFun := fun (z : ℂ) => ↑r / (z - w), is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }

theorem embedding.deriv_ne_zero {U V : Set ℂ} {f : embedding U V} {z : ℂ} (hU : IsOpen U) (hz : z ∈ U) : deriv f.toFun z ≠ 0