Liouville's theorem #

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

In this file we prove Liouville's theorem: if f : E → F is complex differentiable on the whole space and its range is bounded, then the function is a constant. Various versions of this theorem are formalized in differentiable.apply_eq_apply_of_bounded, differentiable.exists_const_forall_eq_of_bounded, and differentiable.exists_eq_const_of_bounded.

The proof is based on the Cauchy integral formula for the derivative of an analytic function, see complex.deriv_eq_smul_circle_integral.

source

theorem complex.deriv_eq_smul_circle_integral {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] [complete_space F] {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R) (hf : diff_cont_on_cl ℂ f (metric.ball c R)) :

deriv f c = (2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ -2 • f z

If f is complex differentiable on an open disc with center c and radius R > 0 and is continuous on its closure, then f' c can be represented as an integral over the corresponding circle.

TODO: add a version for w ∈ metric.ball c R.

TODO: add a version for higher derivatives.

source

theorem complex.norm_deriv_le_aux {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] [complete_space F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) (hf : diff_cont_on_cl ℂ f (metric.ball c R)) (hC : ∀ (z : ℂ), z ∈ metric.sphere c R → ‖f z‖ ≤ C) :

‖deriv f c‖ ≤ C / R

source

theorem complex.norm_deriv_le_of_forall_mem_sphere_norm_le {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) (hd : diff_cont_on_cl ℂ f (metric.ball c R)) (hC : ∀ (z : ℂ), z ∈ metric.sphere c R → ‖f z‖ ≤ C) :

‖deriv f c‖ ≤ C / R

If f is complex differentiable on an open disc of radius R > 0, is continuous on its closure, and its values on the boundary circle of this disc are bounded from above by C, then the norm of its derivative at the center is at most C / R.

source

theorem complex.liouville_theorem_aux {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] {f : ℂ → F} (hf : differentiable ℂ f) (hb : metric.bounded (set.range f)) (z w : ℂ) :

f z = f w

An auxiliary lemma for Liouville's theorem differentiable.apply_eq_apply_of_bounded.

source

theorem differentiable.apply_eq_apply_of_bounded {E : Type u} [normed_add_comm_group E] [normed_space ℂ E] {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] {f : E → F} (hf : differentiable ℂ f) (hb : metric.bounded (set.range f)) (z w : E) :

f z = f w

Liouville's theorem: a complex differentiable bounded function f : E → F is a constant.

source

theorem differentiable.exists_const_forall_eq_of_bounded {E : Type u} [normed_add_comm_group E] [normed_space ℂ E] {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] {f : E → F} (hf : differentiable ℂ f) (hb : metric.bounded (set.range f)) :

∃ (c : F), ∀ (z : E), f z = c

Liouville's theorem: a complex differentiable bounded function is a constant.

source

theorem differentiable.exists_eq_const_of_bounded {E : Type u} [normed_add_comm_group E] [normed_space ℂ E] {F : Type v} [normed_add_comm_group F] [normed_space ℂ F] {f : E → F} (hf : differentiable ℂ f) (hb : metric.bounded (set.range f)) :

∃ (c : F), f = function.const E c

Liouville's theorem: a complex differentiable bounded function is a constant.