# The open mapping theorem for holomorphic functions #

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 `(fun 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 `DiffContOnCl.ball_subset_image_closedBall`

.

## Main results #

`AnalyticAt.eventually_constant_or_nhds_le_map_nhds`

is the local version of the open mapping theorem around a point;`AnalyticOn.is_constant_or_isOpen`

is the open mapping theorem on a connected open set.

If the modulus of a holomorphic function `f`

is bounded below by `ε`

on a circle, then its range
contains a disk of radius `ε / 2`

.

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 `isOpenMap_iff_nhds_le`

). For a function `f : E → ℂ`

the same result holds, see `AnalyticAt.eventually_constant_or_nhds_le_map_nhds`

.

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 `AnalyticAt.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 `ℂ`

).