Liouville's theorem

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_circleIntegral.

theorem Complex.deriv_eq_smul_circleIntegral {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R) (hf : DiffContOnCl ℂ 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.

theorem Complex.norm_deriv_le_aux {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R : ℝ} {C : ℝ} {f : ℂ → F} (hR : 0 < R) (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖deriv f c‖ ≤ C / R

theorem Complex.norm_deriv_le_of_forall_mem_sphere_norm_le {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℂ} {R : ℝ} {C : ℝ} {f : ℂ → F} (hR : 0 < R) (hd : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ 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.

theorem Complex.liouville_theorem_aux {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) (z : ℂ) (w : ℂ) : f z = f w

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

theorem Differentiable.apply_eq_apply_of_bounded {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) (z : E) (w : E) : f z = f w

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

theorem Differentiable.exists_const_forall_eq_of_bounded {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) : ∃ (c : F), ∀ (z : E), f z = c

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

theorem Differentiable.exists_eq_const_of_bounded {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) : ∃ (c : F), f = Function.const E c

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

theorem Differentiable.eq_const_of_tendsto_cocompact {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] {f : E → F} (hf : Differentiable ℂ f) {c : F} (hb : Filter.Tendsto f (Filter.cocompact E) (nhds c)) : f = Function.const E c

A corollary of Liouville's theorem where the function tends to a finite value at infinity (i.e., along Filter.cocompact, which in proper spaces coincides with Bornology.cobounded).

theorem Differentiable.apply_eq_of_tendsto_cocompact {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] {f : E → F} (hf : Differentiable ℂ f) {c : F} (x : E) (hb : Filter.Tendsto f (Filter.cocompact E) (nhds c)) : f x = c

A corollary of Liouville's theorem where the function tends to a finite value at infinity (i.e., along Filter.cocompact, which in proper spaces coincides with Bornology.cobounded).