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;
• AnalyticOnNhd.is_constant_or_isOpen is the open mapping theorem on a connected open set.

As an immediate corollary, we show that a holomorphic function whose real part is constant is itself constant.

theorem DiffContOnCl.ball_subset_image_closedBall {f : ℂ → ℂ} {z₀ : ℂ} {ε r : ℝ} (h : DiffContOnCl ℂ f (Metric.ball z₀ r)) (hr : 0 < r) (hf : ∀ 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.closedBall 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 AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ 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 isOpenMap_iff_nhds_le). For a function f : E → ℂ the same result holds, see AnalyticAt.eventually_constant_or_nhds_le_map_nhds.

theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : E → ℂ} {z₀ : E} (hg : AnalyticAt ℂ 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 AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux.

theorem AnalyticOnNhd.is_constant_or_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) : (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (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 ℂ).

theorem AnalyticOnNhd.is_constant_or_isOpenMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : E → ℂ} (hg : AnalyticOnNhd ℂ g Set.univ) : (∃ (w : ℂ), ∀ (z : E), g z = w) ∨ IsOpenMap g

Holomorphic Functions with Constant Real or Imaginary Part

theorem AnalyticOnNhd.eq_const_of_re_eq_const {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ} (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∀ x ∈ U, (f x).re = c₀) (h₁U : IsOpen U) (h₂U : IsConnected U) : ∃ (c : ℂ), ∀ x ∈ U, f x = c

Corollary to the open mapping theorem: A holomorphic function whose real part is constant is itself constant.

theorem AnalyticOnNhd.eq_re_add_const_mul_I_of_re_eq_const {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ} (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∀ x ∈ U, (f x).re = c₀) (h₁U : IsOpen U) (h₂U : IsConnected U) : ∃ (c : ℝ), ∀ x ∈ U, f x = ↑c₀ + ↑c * Complex.I

Corollary to the open mapping theorem: A holomorphic function whose real part is constant is itself constant.

theorem AnalyticOnNhd.eq_const_of_im_eq_const {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ} (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∀ x ∈ U, (f x).im = c₀) (h₁U : IsOpen U) (h₂U : IsConnected U) : ∃ (c : ℂ), ∀ x ∈ U, f x = c

Corollary to the open mapping theorem: A holomorphic function whose imaginary part is constant is itself constant.

theorem AnalyticOnNhd.eq_const_add_im_mul_I_of_re_eq_const {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ} (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∀ x ∈ U, (f x).im = c₀) (h₁U : IsOpen U) (h₂U : IsConnected U) : ∃ (c : ℝ), ∀ x ∈ U, f x = ↑c + ↑c₀ * Complex.I

Corollary to the open mapping theorem: A holomorphic function whose imaginary part is constant is itself constant.

Holomorphic Functions as Open Quotient Maps

theorem Polynomial.C_eq_or_isOpenQuotientMap_eval (p : Polynomial ℂ) : (∃ (x : ℂ), C x = p) ∨ IsOpenQuotientMap fun (x : ℂ) => eval x p

theorem Polynomial.isOpenQuotientMap_eval (p : Polynomial ℂ) (hp : p.natDegree ≠ 0) : IsOpenQuotientMap fun (x : ℂ) => eval x p

theorem Complex.isOpenQuotientMap_pow (n : ℕ) [NeZero n] : IsOpenQuotientMap fun (x : ℂ) => x ^ n

theorem Complex.isOpenQuotientMap_pow_compl_zero (n : ℕ) [NeZero n] : IsOpenQuotientMap fun (z : { z : ℂ // z ≠ 0 }) => ⟨↑z ^ n, ⋯⟩

theorem Complex.isOpenQuotientMap_zpow_compl_zero (n : ℤ) [NeZero n] : IsOpenQuotientMap fun (z : { z : ℂ // z ≠ 0 }) => ⟨↑z ^ n, ⋯⟩