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.
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.
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 ℂ).