Riemann mapping theorem

TheoremRiemann mapping theorem#✓fully proved

Let \(U\) be a simply connected open subset of \(\mathbb{C}\) with \(U \ne \mathbb{C}\), and let \(z_0 \in U\). Then there is a function \(f : \mathbb{C} \to \mathbb{C}\), holomorphic on \(U\), that maps \(U\) bijectively onto the open unit disc \(\{w : |w| < 1\}\), with \(f(z_0) = 0\) and \(f'(z_0)\) a positive real number. It is unique on \(U\): every function \(g : \mathbb{C} \to \mathbb{C}\) with the same four properties agrees with \(f\) at every point of \(U\).

public theorem riemannMapping_normalized
    {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ Set.univ)
    {z₀ : ℂ} (hz₀ : z₀ ∈ U) :
    ∃ f : ℂ → ℂ, DifferentiableOn ℂ f U ∧ Set.BijOn f U (Metric.ball (0 : ℂ) 1) ∧
      f z₀ = 0 ∧ (deriv f z₀).im = 0 ∧ 0 < (deriv f z₀).re ∧
      ∀ g : ℂ → ℂ, DifferentiableOn ℂ g U → Set.BijOn g U (Metric.ball (0 : ℂ) 1) →
        g z₀ = 0 → (deriv g z₀).im = 0 → 0 < (deriv g z₀).re →
        Set.EqOn f g U

Sources

• same as Riemann mapping; B. Riemann thesis 1851; W. F. Osgood Trans. Amer. Math. Soc. 1 (1900), 310–314, DOI 10.2307/1986285; C. Carathéodory Math. Ann. 72 (1912), 107–144, DOI 10.1007/BF01456892; Ahlfors; Lean adds f z₀=0 positive real derivative via im=0 re>0 and EqOn uniqueness on U.

Uses 3

Proof usesLocally uniformly bounded sequence of functions · A uniformly bounded sequence on an open set is locally uniformly bounded · Montel's theorem

AbbreviationOpen unit disc#✓fully proved

The open unit disc is the set of complex numbers \(z\) with \(|z| < 1\), the open ball of radius \(1\) about \(0\) in \(\mathbb{C}\).

abbrev unitDisk : Set ℂ := Metric.ball (0 : ℂ) 1

Used by 2

Used byAdmissible maps into the unit disc · Existence of an extremal injective map into the unit disc

DefinitionAdmissible maps into the unit disc#✓fully proved

For a set \(\Omega \subseteq \mathbb{C}\), the admissible family of \(\Omega\) is the set of functions \(f : \mathbb{C} \to \mathbb{C}\) that are complex differentiable on \(\Omega\), injective on \(\Omega\), satisfy \(f(0) = 0\), and map \(\Omega\) into the open unit disc \(\{z \in \mathbb{C} : |z| < 1\}\).

def AdmissibleFamily (Ω : Set ℂ) : Set (ℂ → ℂ) :=
  {f | DifferentiableOn ℂ f Ω ∧ Set.InjOn f Ω ∧ f 0 = 0 ∧ Set.MapsTo f Ω unitDisk}

Uses 1 · Used by 1

Statement usesOpen unit disc

Used byExistence of an extremal injective map into the unit disc

TheoremExistence of an extremal injective map into the unit disc#●ready to prove

Let \(D\) be the open unit disc \(\{z \in \mathbb{C} : |z| < 1\}\), let \(\Omega \subseteq D\) be open and connected with \(0 \in \Omega\), and let \(F\) be the family of functions \(f\) that are holomorphic and injective on \(\Omega\), map \(\Omega\) into \(D\), and satisfy \(f(0) = 0\). Then some \(g \in F\) attains the supremum of \(|f'(0)|\) over \(F\):

\[|g'(0)| = \sup_{f \in F} |f'(0)|.\]

public theorem_wanted exists_mem_admissibleFamily_norm_deriv_eq_sSup
  (Ω : Set ℂ)
  (hΩ_open : IsOpen Ω)
  (hΩ_connected : IsConnected Ω)
  (h0 : (0 : ℂ) ∈ Ω)
  (hΩ_subset : Ω ⊆ unitDisk) :
  ∃ g ∈ AdmissibleFamily Ω,
    ‖deriv g 0‖ = sSup ((fun f : ℂ → ℂ => ‖deriv f 0‖) '' AdmissibleFamily Ω)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_22.

Uses 2

Statement usesAdmissible maps into the unit disc · Open unit disc

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.