From d53532461420280db404336ff53f5e8ecf70e54b Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 16 Feb 2022 22:38:59 -0500 Subject: [PATCH 1/5] feat(analysis/complex/liouville): prove Liouville's theorem --- src/analysis/complex/liouville.lean | 106 ++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 src/analysis/complex/liouville.lean diff --git a/src/analysis/complex/liouville.lean b/src/analysis/complex/liouville.lean new file mode 100644 index 0000000000000..735a67216c354 --- /dev/null +++ b/src/analysis/complex/liouville.lean @@ -0,0 +1,106 @@ +/- +Copyright (c) 2022 Yury G. Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury G. Kudryashov +-/ +import analysis.complex.cauchy_integral +import analysis.calculus.fderiv_analytic + +/-! +# 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 `complex.apply_eq_apply_of_differentiable_of_bounded`, +`complex.exists_const_forall_eq_of_differentiable_of_bounded`, and +`complex.exists_eq_const_of_differentiable_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`. +-/ + +open topological_space metric set filter asymptotics function measure_theory +open_locale topological_space filter nnreal real + +universes u v +variables {E : Type u} [normed_group E] [normed_space ℂ E] + {F : Type v} [normed_group F] [normed_space ℂ F] [measurable_space F] [borel_space F] + [second_countable_topology F] [complete_space F] + +namespace complex + +/-- If `f` is complex differentiable on a closed disc with center `c` and radius `R > 0`, 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. -/ +lemma deriv_eq_smul_circle_integral {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R) + (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) : + deriv f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z := +begin + lift R to ℝ≥0 using hR.le, + refine (has_fpower_series_on_ball_of_continuous_on_of_differentiable_on + hc hd hR).has_fpower_series_at.deriv.trans _, + simp only [cauchy_power_series_apply, one_div, zpow_neg₀, pow_one, smul_smul, + zpow_two, mul_inv₀] +end + +/-- If `f` is continuous on a closed disc of radius `R`, is complex differentiable on its interior, +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`. + +TODO: drop unneeded assumptions `[complete_space F] [second_countable_topology F]`. -/ +lemma norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) + (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) + (hC : ∀ z ∈ sphere c R, ∥f z∥ ≤ C) : + ∥deriv f c∥ ≤ C / R := +have ∀ z ∈ sphere c R, ∥(z - c) ^ (-2 : ℤ) • f z∥ ≤ C / (R * R), + from λ z (hz : abs (z - c) = R), by simpa [norm_smul, hz, zpow_two, ← div_eq_inv_mul] + using (div_le_div_right (mul_pos hR hR)).2 (hC z hz), +calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z∥ : + congr_arg norm (deriv_eq_smul_circle_integral hR hc hd) +... ≤ R * (C / (R * R)) : + circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const hR.le this +... = C / R : by rw [mul_div_comm, div_self_mul_self', div_eq_mul_inv] + +/-- **Liouville's theorem**: a complex differentiable bounded function `f : ℂ → E` is a constant. +Use a more general `complex.apply_eq_apply_of_differentiable_of_bounded` instead. -/ +lemma apply_eq_apply_of_differentiable_of_bounded_dim1 {f : ℂ → F} (hf : differentiable ℂ f) + (hb : bounded (range f)) (z w : ℂ) : f z = f w := +begin + suffices : ∀ c, deriv f c = 0, from is_const_of_deriv_eq_zero hf this z w, + clear z w, intro c, + obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ∥f z∥ ≤ C, + { rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩, + exact ⟨max C 1, lt_max_iff.2 (or.inr zero_lt_one), + λ z, (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩ }, + refine norm_le_zero_iff.1 (le_of_forall_le_of_dense $ λ ε ε₀, _), + calc ∥deriv f c∥ ≤ C / (C / ε) : + norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.continuous.continuous_on + hf.differentiable_on (λ z _, hC z) + ... = ε : div_div_cancel' C₀.lt.ne' +end + +/-- **Liouville's theorem**: a complex differentiable bounded function `f : E → F` is a constant. -/ +lemma apply_eq_apply_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) + (hb : bounded (range f)) (z w : E) : f z = f w := +begin + set g : ℂ → F := f ∘ (λ t : ℂ, t • (w - z) + z), + suffices : g 0 = g 1, by simpa [g], + apply apply_eq_apply_of_differentiable_of_bounded_dim1, + exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z), + hb.mono (range_comp_subset_range _ _)] +end + +/-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/ +lemma exists_const_forall_eq_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) + (hb : bounded (range f)) : ∃ c, ∀ z, f z = c := +⟨f 0, λ z, apply_eq_apply_of_differentiable_of_bounded hf hb _ _⟩ + +/-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/ +lemma exists_eq_const_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) + (hb : bounded (range f)) : ∃ c, f = const E c := +(exists_const_forall_eq_of_differentiable_of_bounded hf hb).imp $ λ c, funext + +end complex From c6e42f02ecb8020eb2f8f1503282e5ac098ac8e0 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 18 Feb 2022 15:43:22 -0500 Subject: [PATCH 2/5] Move to the `differentiable` NS --- src/analysis/complex/liouville.lean | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/src/analysis/complex/liouville.lean b/src/analysis/complex/liouville.lean index 735a67216c354..5a8da3b2c2adb 100644 --- a/src/analysis/complex/liouville.lean +++ b/src/analysis/complex/liouville.lean @@ -66,7 +66,7 @@ calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) /-- **Liouville's theorem**: a complex differentiable bounded function `f : ℂ → E` is a constant. Use a more general `complex.apply_eq_apply_of_differentiable_of_bounded` instead. -/ -lemma apply_eq_apply_of_differentiable_of_bounded_dim1 {f : ℂ → F} (hf : differentiable ℂ f) +lemma liouville_theorem_aux {f : ℂ → F} (hf : differentiable ℂ f) (hb : bounded (range f)) (z w : ℂ) : f z = f w := begin suffices : ∀ c, deriv f c = 0, from is_const_of_deriv_eq_zero hf this z w, @@ -82,25 +82,31 @@ begin ... = ε : div_div_cancel' C₀.lt.ne' end +end complex + +namespace differentiable + +open complex + /-- **Liouville's theorem**: a complex differentiable bounded function `f : E → F` is a constant. -/ -lemma apply_eq_apply_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) - (hb : bounded (range f)) (z w : E) : f z = f w := +lemma apply_eq_apply_of_bounded {f : E → F} (hf : differentiable ℂ f) (hb : bounded (range f)) + (z w : E) : f z = f w := begin set g : ℂ → F := f ∘ (λ t : ℂ, t • (w - z) + z), suffices : g 0 = g 1, by simpa [g], - apply apply_eq_apply_of_differentiable_of_bounded_dim1, + apply liouville_theorem_aux, exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z), hb.mono (range_comp_subset_range _ _)] end /-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/ -lemma exists_const_forall_eq_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) +lemma exists_const_forall_eq_of_bounded {f : E → F} (hf : differentiable ℂ f) (hb : bounded (range f)) : ∃ c, ∀ z, f z = c := -⟨f 0, λ z, apply_eq_apply_of_differentiable_of_bounded hf hb _ _⟩ +⟨f 0, λ z, hf.apply_eq_apply_of_bounded hb _ _⟩ /-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/ -lemma exists_eq_const_of_differentiable_of_bounded {f : E → F} (hf : differentiable ℂ f) +lemma exists_eq_const_of_bounded {f : E → F} (hf : differentiable ℂ f) (hb : bounded (range f)) : ∃ c, f = const E c := -(exists_const_forall_eq_of_differentiable_of_bounded hf hb).imp $ λ c, funext +(hf.exists_const_forall_eq_of_bounded hb).imp $ λ c, funext -end complex +end differentiable From d52b0adb5dbd53a9dbccf72c803fcccac112e462 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 18 Feb 2022 15:44:48 -0500 Subject: [PATCH 3/5] Fix docstrings --- src/analysis/complex/liouville.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analysis/complex/liouville.lean b/src/analysis/complex/liouville.lean index 5a8da3b2c2adb..8bdabc489978e 100644 --- a/src/analysis/complex/liouville.lean +++ b/src/analysis/complex/liouville.lean @@ -11,9 +11,9 @@ import analysis.calculus.fderiv_analytic 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 `complex.apply_eq_apply_of_differentiable_of_bounded`, -`complex.exists_const_forall_eq_of_differentiable_of_bounded`, and -`complex.exists_eq_const_of_differentiable_of_bounded`. +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`. @@ -65,7 +65,7 @@ calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ... = C / R : by rw [mul_div_comm, div_self_mul_self', div_eq_mul_inv] /-- **Liouville's theorem**: a complex differentiable bounded function `f : ℂ → E` is a constant. -Use a more general `complex.apply_eq_apply_of_differentiable_of_bounded` instead. -/ +Use a more general `differentiable.apply_eq_apply_of_bounded` instead. -/ lemma liouville_theorem_aux {f : ℂ → F} (hf : differentiable ℂ f) (hb : bounded (range f)) (z w : ℂ) : f z = f w := begin From 078fad3cf12f68eacccbc4a1ca75d23fe09c8397 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 18 Feb 2022 15:45:46 -0500 Subject: [PATCH 4/5] Fix another docstring --- src/analysis/complex/liouville.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analysis/complex/liouville.lean b/src/analysis/complex/liouville.lean index 8bdabc489978e..6b1ba8e2482cb 100644 --- a/src/analysis/complex/liouville.lean +++ b/src/analysis/complex/liouville.lean @@ -64,8 +64,7 @@ calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const hR.le this ... = C / R : by rw [mul_div_comm, div_self_mul_self', div_eq_mul_inv] -/-- **Liouville's theorem**: a complex differentiable bounded function `f : ℂ → E` is a constant. -Use a more general `differentiable.apply_eq_apply_of_bounded` instead. -/ +/-- An auxiliary lemma for Liouville's theorem `differentiable.apply_eq_apply_of_bounded`. -/ lemma liouville_theorem_aux {f : ℂ → F} (hf : differentiable ℂ f) (hb : bounded (range f)) (z w : ℂ) : f z = f w := begin From 1d7ba57924036118fba6b2c8ce52ec4affbad36d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 26 Feb 2022 22:30:57 -0500 Subject: [PATCH 5/5] Snapshot --- src/analysis/complex/liouville.lean | 47 +++++++++++++++++++++-------- 1 file changed, 35 insertions(+), 12 deletions(-) diff --git a/src/analysis/complex/liouville.lean b/src/analysis/complex/liouville.lean index 6b1ba8e2482cb..cb7209176b1d1 100644 --- a/src/analysis/complex/liouville.lean +++ b/src/analysis/complex/liouville.lean @@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov -/ import analysis.complex.cauchy_integral import analysis.calculus.fderiv_analytic +import analysis.normed_space.completion /-! # Liouville's theorem @@ -24,8 +25,9 @@ open_locale topological_space filter nnreal real universes u v variables {E : Type u} [normed_group E] [normed_space ℂ E] - {F : Type v} [normed_group F] [normed_space ℂ F] [measurable_space F] [borel_space F] - [second_countable_topology F] [complete_space F] + {F : Type v} [normed_group F] [normed_space ℂ F] [second_countable_topology F] + +local postfix `̂`:100 := uniform_space.completion namespace complex @@ -35,7 +37,8 @@ namespace complex TODO: add a version for `w ∈ metric.ball c R`. TODO: add a version for higher derivatives. -/ -lemma deriv_eq_smul_circle_integral {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R) +lemma deriv_eq_smul_circle_integral [measurable_space F] [borel_space F] [complete_space F] + {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R) (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) : deriv f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z := begin @@ -46,23 +49,43 @@ begin zpow_two, mul_inv₀] end +lemma norm_deriv_le_aux [complete_space F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) + (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) + (hC : ∀ z ∈ sphere c R, ∥f z∥ ≤ C) : + ∥deriv f c∥ ≤ C / R := +begin + letI : measurable_space F := borel F, haveI : borel_space F := ⟨rfl⟩, + have : ∀ z ∈ sphere c R, ∥(z - c) ^ (-2 : ℤ) • f z∥ ≤ C / (R * R), + from λ z (hz : abs (z - c) = R), by simpa [norm_smul, hz, zpow_two, ← div_eq_inv_mul] + using (div_le_div_right (mul_pos hR hR)).2 (hC z hz), + calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z∥ : + congr_arg norm (deriv_eq_smul_circle_integral hR hc hd) + ... ≤ R * (C / (R * R)) : + circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const hR.le this + ... = C / R : by rw [mul_div_comm, div_self_mul_self', div_eq_mul_inv] +end + /-- If `f` is continuous on a closed disc of radius `R`, is complex differentiable on its interior, 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`. -TODO: drop unneeded assumptions `[complete_space F] [second_countable_topology F]`. -/ +TODO: drop unneeded assumption `[second_countable_topology F]`. -/ lemma norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ∥f z∥ ≤ C) : ∥deriv f c∥ ≤ C / R := -have ∀ z ∈ sphere c R, ∥(z - c) ^ (-2 : ℤ) • f z∥ ≤ C / (R * R), - from λ z (hz : abs (z - c) = R), by simpa [norm_smul, hz, zpow_two, ← div_eq_inv_mul] - using (div_le_div_right (mul_pos hR hR)).2 (hC z hz), -calc ∥deriv f c∥ = ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z∥ : - congr_arg norm (deriv_eq_smul_circle_integral hR hc hd) -... ≤ R * (C / (R * R)) : - circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const hR.le this -... = C / R : by rw [mul_div_comm, div_self_mul_self', div_eq_mul_inv] +begin + haveI : second_countable_topology (F̂) := uniform_space.second_countable_of_separable _, + set e : F →L[ℂ] F̂ := uniform_space.completion.to_complL, + have : has_deriv_at (e ∘ f) (e (deriv f c)) c, + from e.has_fderiv_at.comp_has_deriv_at c (hd.has_deriv_at $ ball_mem_nhds _ hR), + calc ∥deriv f c∥ = ∥deriv (e ∘ f) c∥ : + by { rw this.deriv, exact (uniform_space.completion.norm_coe _).symm } + ... ≤ C / R : + norm_deriv_le_aux hR (e.continuous.comp_continuous_on hc) + (e.differentiable.comp_differentiable_on hd) + (λ z hz, (uniform_space.completion.norm_coe _).trans_le (hC z hz)) +end /-- An auxiliary lemma for Liouville's theorem `differentiable.apply_eq_apply_of_bounded`. -/ lemma liouville_theorem_aux {f : ℂ → F} (hf : differentiable ℂ f)