Geometric function theory

Conformal and univalent maps: Riemann mapping, Koebe and Bloch theorems, Schwarz–Pick and half-plane self-maps, starlike and univalent coefficient problems, Loewner equation, holomorphic motions.

TheoremA Möbius map from the unit disk onto the upper half-plane#●ready to prove

The function \(\phi(z) = i\,\frac{1-z}{1+z}\) maps the open unit disk \(D = \{z \in \mathbb{C} : |z| < 1\}\) bijectively onto the upper half-plane \(U = \{z \in \mathbb{C} : \operatorname{Im} z > 0\}\): it maps \(D\) into \(U\), it is injective on \(D\), and every point of \(U\) is \(\phi(z)\) for some \(z \in D\).

public theorem_wanted bijOn_cayley_ball_upperHalfPlane
    (φ : ℂ → ℂ) (hφ : φ = fun z : ℂ => Complex.I * (1 - z) / (1 + z)) :
    Set.BijOn φ (Metric.ball (0 : ℂ) 1) {w : ℂ | 0 < w.im}
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l1_63.

TheoremBloch's theorem#✓fully proved

There is a constant \(B > 0\) with the following property. Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the open unit disc \(\mathbb{D} = \{z : |z| < 1\}\) with \(f'(0) = 1\). Then there are an open connected set \(V \subseteq \mathbb{D}\) and a point \(w \in \mathbb{C}\) such that \(f\) is injective on \(V\) and \(f(V)\) is the open disc \(\{\zeta : |\zeta - w| < B\}\).

theorem bloch
    : ∃ B : ℝ, 0 < B ∧
      ∀ f : ℂ → ℂ, DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1) → deriv f 0 = 1 →
        ∃ V : Set ℂ, ∃ w : ℂ,
          IsOpen V ∧ V ⊆ Metric.ball (0 : ℂ) 1 ∧ IsConnected V ∧
            Set.InjOn f V ∧ f '' V = Metric.ball w B
Sources
  • A. Bloch, Les théorèmes de M. Valiron sur les fonctions entières et la théorie de l'uniformisation, Ann. Fac. Sci. Toulouse 17 (1925), 1–22, DOI 10.5802/afst.335; see Ahlfors, Complex Analysis, Univalent Functions; Lean is universal B > 0 exact schlicht disc f '' V = ball w B for open connected V, stronger than Landau.
Used by 1
Used byGreat Picard theorem

TheoremDiameter bound for the derivative at the center of the disc#●ready to prove

Let \(D\) be the open unit disc in \(\mathbb{C}\) and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on \(D\). Then the diameter \(d = \sup_{z,w \in D} |f(z) - f(w)|\) of the image \(f(D)\), which may be \(+\infty\), satisfies \(2|f'(0)| \le d\).

public theorem_wanted two_mul_norm_deriv_le_ediam_image_ball
    (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1)) :
    ENNReal.ofReal (2 * ‖deriv f 0‖) ≤ Metric.ediam (f '' (Metric.ball (0 : ℂ) 1))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_78.

TheoremNo proper holomorphic map from the unit disc to the complex plane#●ready to prove

Let \(\Delta := \{z\in\mathbb{C}\mid |z|<1\}\) be the unit disc in the complex plane. There is no proper holomorphic map \(f:\Delta\to\mathbb{C}\), where proper means that the preimage under \(f\) of every compact subset of \(\mathbb{C}\) is a compact subset of \(\Delta\).

public theorem_wanted not_exists_differentiableOn_ball_isCompact_preimage :
    ¬ ∃ f : ℂ → ℂ,
        DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1) ∧
          (∀ K : Set ℂ, IsCompact K →
            IsCompact ((fun z : Metric.ball (0 : ℂ) 1 => f z) ⁻¹' K))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_41.

TheoremNonconstant holomorphic functions of modulus one on the unit circle cover the unit disc#●ready to prove

Let \(U\subseteq\mathbb{C}\) be a connected open set containing the closed unit disc \(\{z:|z|\le 1\}\), and let \(f:\mathbb{C}\to\mathbb{C}\) be holomorphic on \(U\) and non-constant on \(U\). If \(|f(z)|=1\) whenever \(|z|=1\), then every \(w\) with \(|w|<1\) is \(f(z)\) for some \(z\in U\); that is, \(f(U)\) contains the open unit disc.

The connectedness of \(U\) is added to the source statement, which asks only for an open set: for \(U=\{z:|z|<2\}\cup\{z:|z-10|<1\}\), with \(f=1\) on the first disc and \(f(z)=z\) on the second, \(f\) is non-constant and holomorphic on \(U\) and has modulus one on the unit circle, but \(f(U)\) does not contain the open unit disc.

public theorem_wanted ball_subset_image_of_norm_eq_one_on_sphere {f : ℂ → ℂ} {U : Set ℂ}
    (hU : IsOpen U) (hUconn : IsPreconnected U)
    (hclosed : Metric.closedBall (0 : ℂ) 1 ⊆ U)
    (hf : DifferentiableOn ℂ f U)
    (hnonconst : ∃ z₁ ∈ U, ∃ z₂ ∈ U, f z₁ ≠ f z₂)
    (hboundary : ∀ z, z ∈ Metric.sphere (0 : ℂ) 1 → ‖f z‖ = 1) :
    Metric.ball (0 : ℂ) 1 ⊆ f '' U
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_25, with the change above.
1 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.