From 66ec15ccd109e82ef80c4340ab86cef6b26c7ebd Mon Sep 17 00:00:00 2001 From: frankymacster Date: Wed, 26 May 2021 13:34:25 +0000 Subject: [PATCH] feat(analysis/complex/isometry): add linear_isometry_complex (#6923) add proof about the isometries in the complex plane Co-authored-by: frankymacster Co-authored-by: Floris van Doorn --- src/analysis/complex/basic.lean | 2 + src/analysis/complex/isometry.lean | 152 ++++++++++++++++++ .../normed_space/linear_isometry.lean | 7 + src/data/complex/basic.lean | 5 + 4 files changed, 166 insertions(+) create mode 100644 src/analysis/complex/isometry.lean diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean index d07602c2ed400..13222c7077f71 100644 --- a/src/analysis/complex/basic.lean +++ b/src/analysis/complex/basic.lean @@ -106,6 +106,8 @@ calc 1 = ∥im_clm I∥ : by simp /-- The complex-conjugation function from `ℂ` to itself is an isometric linear map. -/ def conj_li : ℂ →ₗᵢ[ℝ] ℂ := ⟨conj_lm, λ x, by simp⟩ +@[simp] lemma conj_li_apply (z : ℂ) : conj_li z = conj_lm z := rfl + /-- Continuous linear map version of the conj function, from `ℂ` to `ℂ`. -/ def conj_clm : ℂ →L[ℝ] ℂ := conj_li.to_continuous_linear_map diff --git a/src/analysis/complex/isometry.lean b/src/analysis/complex/isometry.lean new file mode 100644 index 0000000000000..3d8959b7db9c0 --- /dev/null +++ b/src/analysis/complex/isometry.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2021 François Sunatori. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: François Sunatori +-/ +import analysis.complex.basic +import data.complex.exponential +import data.real.sqrt +import analysis.normed_space.linear_isometry +import algebra.group.units + +/-! +# Isometries of the Complex Plane + +The lemma `linear_isometry_complex` states the classification of isometries in the complex plane. +Specifically, isometries with rotations but without translation. +The proof involves: +1. creating a linear isometry `g` with two fixed points, `g(0) = 0`, `g(1) = 1` +2. applying `linear_isometry_complex_aux` to `g` +The proof of `linear_isometry_complex_aux` is separated in the following parts: +1. show that the real parts match up: `linear_isometry.re_apply_eq_re` +2. show that I maps to either I or -I +3. every z is a linear combination of a + b * I + +## References + +* [Isometries of the Complex Plane](http://helmut.knaust.info/mediawiki/images/b/b5/Iso.pdf) +-/ +noncomputable theory + +open complex + +local notation `|` x `|` := complex.abs x + +lemma linear_isometry.re_apply_eq_re_of_add_conj_eq (f : ℂ →ₗᵢ[ℝ] ℂ) + (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re := +by simpa [ext_iff, add_re, add_im, conj_re, conj_im, ←two_mul, + (show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm + +lemma linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} + (h₁ : ∀ z, |f z| = |z|) (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) : + (f z).im = z.im ∨ (f z).im = -z.im := +begin + specialize h₁ z, + simp only [complex.abs] at h₁, + rwa [real.sqrt_inj (norm_sq_nonneg _) (norm_sq_nonneg _), norm_sq_apply (f z), norm_sq_apply z, + h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁, +end + +lemma linear_isometry.abs_apply_sub_one_eq_abs_sub_one {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : + ∥f z - 1∥ = ∥z - 1∥ := +by rw [←linear_isometry.norm_map f (z - 1), linear_isometry.map_sub, h] + +lemma linear_isometry.im_apply_eq_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : + z + conj z = f z + conj (f z) := +begin + have := linear_isometry.abs_apply_sub_one_eq_abs_sub_one h z, + apply_fun λ x, x ^ 2 at this, + simp only [norm_eq_abs, ←norm_sq_eq_abs] at this, + rw [←of_real_inj, ←mul_conj, ←mul_conj] at this, + rw [conj.map_sub, conj.map_sub] at this, + simp only [sub_mul, mul_sub, one_mul, mul_one] at this, + rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs, linear_isometry.norm_map] at this, + rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs] at this, + simp only [sub_sub, sub_right_inj, mul_one, of_real_pow, ring_hom.map_one, norm_eq_abs] at this, + simp only [add_sub, sub_left_inj] at this, + rw [add_comm, ←this, add_comm], +end + +lemma linear_isometry.re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : (f z).re = z.re := +begin + apply linear_isometry.re_apply_eq_re_of_add_conj_eq, + intro z, + apply linear_isometry.im_apply_eq_im h, +end + +lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) : + (∀ z, f z = z) ∨ (∀ z, f z = conj z) := +begin + have h0 : f I = I ∨ f I = -I, + { have : |f I| = 1, + { rw [←norm_eq_abs, linear_isometry.norm_map, norm_eq_abs, abs_I] }, + simp only [ext_iff, ←and_or_distrib_left, neg_re, I_re, neg_im, neg_zero], + split, + { rw ←I_re, + rw linear_isometry.re_apply_eq_re h }, + { apply linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re, + { intro z, rw [←norm_eq_abs, ←norm_eq_abs, linear_isometry.norm_map] }, + { intro z, rw linear_isometry.re_apply_eq_re h } } }, + refine or.imp (λ h1, _) (λ h1 z, _) h0, + { suffices : f.to_linear_map = linear_isometry.id.to_linear_map, + { simp [this, ←linear_isometry.coe_to_linear_map, linear_map.id_apply] }, + apply basis.ext basis_one_I, + intro i, + fin_cases i, + { simp [h] }, + { simp only [matrix.head_cons, linear_isometry.coe_to_linear_map, + linear_map.id_coe, id.def, matrix.cons_val_one], simpa } }, + { suffices : f.to_linear_map = conj_li.to_linear_map, + { rw [←linear_isometry.coe_to_linear_map, this], + simp only [linear_isometry.coe_to_linear_map], refl }, + apply basis.ext basis_one_I, + intro i, + fin_cases i, + { simp only [h, linear_isometry.coe_to_linear_map, matrix.cons_val_zero], simpa }, + { simp only [matrix.head_cons, linear_isometry.coe_to_linear_map, + linear_map.id_coe, id.def, matrix.cons_val_one], simpa } }, +end + +lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) : + ∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z)) := +begin + let a := f 1, + use a, + split, + { simp only [← norm_eq_abs, a, linear_isometry.norm_map, norm_one] }, + { let g : ℂ →ₗᵢ[ℝ] ℂ := + { to_fun := λ z, a⁻¹ * f z, + map_add' := by { + intros x y, + rw linear_isometry.map_add, + rw mul_add }, + map_smul' := by { + intros m x, + rw linear_isometry.map_smul, + rw algebra.mul_smul_comm }, + norm_map' := by { + intros x, + simp, + suffices : ∥f 1∥⁻¹ * ∥f x∥ = ∥x∥, { simpa }, + iterate 2 { rw linear_isometry.norm_map }, + simp } }, + have hg1 : g 1 = 1 := by { + change a⁻¹ * a = 1, + rw inv_mul_cancel, + rw ← norm_sq_pos, + rw norm_sq_eq_abs, + change 0 < ∥a∥ ^ 2, + rw linear_isometry.norm_map, + simp, + simp [zero_lt_one] }, + have h : (∀ z, g z = z) ∨ (∀ z, g z = conj z) := linear_isometry_complex_aux g hg1, + change (∀ z, a⁻¹ * f z = z) ∨ (∀ z, a⁻¹ * f z = conj z) at h, + have ha : a ≠ 0 := by { + rw ← norm_sq_pos, + rw norm_sq_eq_abs, + change 0 < ∥a∥ ^ 2, + rw linear_isometry.norm_map, + simp, + simp [zero_lt_one] }, + simpa only [← inv_mul_eq_iff_eq_mul' ha] } +end diff --git a/src/analysis/normed_space/linear_isometry.lean b/src/analysis/normed_space/linear_isometry.lean index f2524114a524e..ece2c2e8a30c1 100644 --- a/src/analysis/normed_space/linear_isometry.lean +++ b/src/analysis/normed_space/linear_isometry.lean @@ -329,4 +329,11 @@ e.isometry.comp_continuous_on_iff continuous (e ∘ f) ↔ continuous f := e.isometry.comp_continuous_iff +@[simp] +lemma linear_isometry.id_apply (x : E) : (linear_isometry.id : E →ₗᵢ[R] E) x = x := rfl + +@[simp] +lemma linear_isometry.id_to_linear_map : + (linear_isometry.id.to_linear_map : E →ₗ[R] E) = linear_map.id := rfl + end linear_isometry_equiv diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean index da4305a178b45..a9dc4aa5e6753 100644 --- a/src/data/complex/basic.lean +++ b/src/data/complex/basic.lean @@ -192,6 +192,11 @@ lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r := lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z := eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩ + +lemma conj_sub (z z': ℂ) : conj (z - z') = conj z - conj z' := conj.map_sub z z' + +lemma conj_one : conj 1 = 1 := by rw conj.map_one + lemma eq_conj_iff_im {z : ℂ} : conj z = z ↔ z.im = 0 := ⟨λ h, add_self_eq_zero.mp (neg_eq_iff_add_eq_zero.mp (congr_arg im h)), λ h, ext rfl (neg_eq_iff_add_eq_zero.mpr (add_self_eq_zero.mpr h))⟩