Great Picard theorem

DefinitionEssential isolated singularity#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) has an essential isolated singularity at \(c \in \mathbb{C}\) when \(f\) is holomorphic on some punctured disc \(0 < |z - c| < r\) with \(r > 0\), \(f(z)\) has no finite limit as \(z \to c\) with \(z \ne c\), and \(|f(z)|\) does not tend to \(\infty\) as \(z \to c\) with \(z \ne c\).

def IsEssentialIsolatedSingularityAt (f : ℂ → ℂ) (c : ℂ) : Prop :=
  (∃ r : ℝ, 0 < r ∧ DifferentiableOn ℂ f (Metric.ball c r \ {c})) ∧
  ¬ (∃ l : ℂ, Tendsto f (𝓝[≠] c) (𝓝 l)) ∧
  ¬ Tendsto (fun z => ‖f z‖) (𝓝[≠] c) Filter.atTop

Used by 1

Used byGreat Picard theorem

TheoremGreat Picard theorem#✓fully proved

Suppose \(f : \mathbb{C} \to \mathbb{C}\) has an essential isolated singularity at \(c \in \mathbb{C}\). Then there is at most one \(w \in \mathbb{C}\) for which some \(r > 0\) makes the set \(\{z : 0 < |z - c| < r,\ f(z) = w\}\) finite; that is, with at most one exception, \(f\) takes every complex value infinitely often on every punctured disc around \(c\).

theorem greatPicard
    {f : ℂ → ℂ} {c : ℂ} (hf : IsEssentialIsolatedSingularityAt f c) :
    Set.Subsingleton
      {w : ℂ | ∃ r : ℝ, 0 < r ∧ Set.Finite {z ∈ Metric.ball c r \ {c} | f z = w}}

Sources

• Great Picard theorem, E. Picard 1879; see Ahlfors, Complex Analysis; Lean is essential isolated singularity version with finite-fiber exceptional set subsingleton, at most one value finitely often near c.

Uses 2

Statement usesEssential isolated singularity

Proof usesBloch's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.