mathlib3 documentation

analysis.complex.open_mapping

The open mapping theorem for holomorphic functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the open mapping theorem for holomorphic functions, namely that an analytic function on a preconnected set of the complex plane is either constant or open. The main step is to show a local version of the theorem that states that if f is analytic at a point z₀, then either it is constant in a neighborhood of z₀ or it maps any neighborhood of z₀ to a neighborhood of its image f z₀. The results extend in higher dimension to g : E → ℂ.

The proof of the local version on goes through two main steps: first, assuming that the function is not constant around z₀, use the isolated zero principle to show that ‖f z‖ is bounded below on a small sphere z₀ r around z₀, and then use the maximum principle applied to the auxiliary function (λ z, ‖f z - v‖) to show that any v close enough to f z₀ is in f '' ball z₀ r. That second step is implemented in diff_cont_on_cl.ball_subset_image_closed_ball.

Main results #

theorem diff_cont_on_cl.ball_subset_image_closed_ball {f : } {z₀ : } {ε r : } (h : diff_cont_on_cl f (metric.ball z₀ r)) (hr : 0 < r) (hf : (z : ), z metric.sphere z₀ r ε f z - f z₀) (hz₀ : ∃ᶠ (z : ) in nhds z₀, f z f z₀) :
metric.ball (f z₀) / 2) f '' metric.closed_ball z₀ r

If the modulus of a holomorphic function f is bounded below by ε on a circle, then its range contains a disk of radius ε / 2.

theorem analytic_at.eventually_constant_or_nhds_le_map_nhds_aux {f : } {z₀ : } (hf : analytic_at f z₀) :
(∀ᶠ (z : ) in nhds z₀, f z = f z₀) nhds (f z₀) filter.map f (nhds z₀)

A function f : ℂ → ℂ which is analytic at a point z₀ is either constant in a neighborhood of z₀, or behaves locally like an open function (in the sense that the image of every neighborhood of z₀ is a neighborhood of f z₀, as in is_open_map_iff_nhds_le). For a function f : E → ℂ the same result holds, see analytic_at.eventually_constant_or_nhds_le_map_nhds.

theorem analytic_at.eventually_constant_or_nhds_le_map_nhds {E : Type u_1} [normed_add_comm_group E] [normed_space E] {g : E } {z₀ : E} (hg : analytic_at g z₀) :
(∀ᶠ (z : E) in nhds z₀, g z = g z₀) nhds (g z₀) filter.map g (nhds z₀)

The open mapping theorem for holomorphic functions, local version: is a function g : E → ℂ is analytic at a point z₀, then either it is constant in a neighborhood of z₀, or it maps every neighborhood of z₀ to a neighborhood of z₀. For the particular case of a holomorphic function on , see analytic_at.eventually_constant_or_nhds_le_map_nhds_aux.

theorem analytic_on.is_constant_or_is_open {E : Type u_1} [normed_add_comm_group E] [normed_space E] {U : set E} {g : E } (hg : analytic_on g U) (hU : is_preconnected U) :
( (w : ), (z : E), z U g z = w) (s : set E), s U is_open s is_open (g '' s)

The open mapping theorem for holomorphic functions, global version: if a function g : E → ℂ is analytic on a connected set U, then either it is constant on U, or it is open on U (in the sense that it maps any open set contained in U to an open set in ).