Koebe quarter theorem

TheoremKoebe quarter theorem#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic and injective on the open unit disk \(\mathbb{D} = \{z : |z| < 1\}\), with \(f(0) = 0\) and \(f'(0) = 1\). Then the image \(f(\mathbb{D})\) contains the open disk \(\{w : |w| < 1/4\}\).

theorem koebe_quarter
    (f : ℂ → ℂ)
    (hf : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1))
    (hinj : Set.InjOn f (Metric.ball (0 : ℂ) 1))
    (h0 : f 0 = 0)
    (hderiv : deriv f 0 = 1) :
    Metric.ball (0 : ℂ) (1/4 : ℝ) ⊆ f '' Metric.ball (0 : ℂ) 1

Sources

• Koebe quarter theorem, conjectured by P. Koebe in 1907 and proved by L. Bieberbach, Sitzungsberichte der Preussischen Akademie der Wissenschaften (1916), 940–955; see Pommerenke, Univalent Functions; Lean is normalized schlicht inclusion ball (0:ℂ) (1/4) ⊆ f '' ball 0 1.

TheoremThe boundary of a normalized univalent image of the disc is within distance one of the origin#●ready to prove

The boundary of a normalized univalent image of the disc is within distance one of the origin. Let \(D=\{z\in\mathbb{C}:|z|<1\}\) be the unit disk and suppose \(f:D\to\mathbb{C}\) is an injective holomorphic function with \(f(0)=0\) and \(f'(0)=1\). Let \(\Omega=f(D)\) and let \(\partial\Omega\) be its boundary. Then \(\mathrm{dist}(0,\partial\Omega)=\inf\{|z|:z\in\partial\Omega\}\le 1\).

public theorem_wanted infDist_zero_frontier_image_ball_le_one
  (f : ℂ → ℂ) (hf_holo : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1))
  (hf_inj : Set.InjOn f (Metric.ball (0 : ℂ) 1)) (hf0 : f 0 = 0) (hf'0 : deriv f 0 = 1) :
  Metric.infDist (0 : ℂ) (frontier (f '' (Metric.ball (0 : ℂ) 1))) ≤ 1

Sources

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

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.