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.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (n : ℕ) (hR : 0 < R) (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖iteratedDeriv n f c‖ ≤ ↑n.factorial * C / R ^ n

Cauchy's estimate for derivatives: 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 n-th derivative at the center is at most n.factorial * C / R ^ n.

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

Cauchy's estimate for the first order derivative: 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. Note that this theorem does not require the completeness of the codomain of f. In constrast, the completeness is needed for norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le.

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