refactor(analysis/normed_space/conformal_linear_map): redefine (#13143)

Use equality of bundled maps instead of coercions to functions in the definition of `is_conformal_map`. Also golf some proofs.

Author: urkud

src/analysis/calculus/conformal/normed_space.lean

@@ -61,22 +61,22 @@ lemma conformal_at_const_smul {c : ℝ} (h : c ≠ 0) (x : X) :
 ⟨c • continuous_linear_map.id ℝ X,
   (has_fderiv_at_id x).const_smul c, is_conformal_map_const_smul h⟩
 
+@[nontriviality] lemma subsingleton.conformal_at [subsingleton X] (f : X → Y) (x : X) :
+  conformal_at f x :=
+⟨0, has_fderiv_at_of_subsingleton _ _, is_conformal_map_of_subsingleton _⟩
+
 /-- A function is a conformal map if and only if its differential is a conformal linear map-/
 lemma conformal_at_iff_is_conformal_map_fderiv {f : X → Y} {x : X} :
   conformal_at f x ↔ is_conformal_map (fderiv ℝ f x) :=
 begin
   split,
-  { rintros ⟨c, hf, hf'⟩,
-    rw hf.fderiv,
-    exact hf' },
+  { rintros ⟨f', hf, hf'⟩,
+    rwa hf.fderiv },
   { intros H,
     by_cases h : differentiable_at ℝ f x,
     { exact ⟨fderiv ℝ f x, h.has_fderiv_at, H⟩, },
-    { cases subsingleton_or_nontrivial X with w w; resetI,
-      { exact ⟨(0 : X →L[ℝ] Y), has_fderiv_at_of_subsingleton f x,
-        is_conformal_map_of_subsingleton 0⟩, },
-      { exfalso,
-        exact H.ne_zero (fderiv_zero_of_not_differentiable_at h), }, }, },
+    { nontriviality X,
+      exact absurd (fderiv_zero_of_not_differentiable_at h) H.ne_zero } },
 end
 
 namespace conformal_at

src/analysis/complex/conformal.lean

@@ -42,8 +42,8 @@ section conformal_into_complex_normed
 variables {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
   {z : ℂ} {g : ℂ →L[ℝ] E} {f : ℂ → E}
 
-lemma is_conformal_map_complex_linear
-  {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : is_conformal_map (map.restrict_scalars ℝ) :=
+lemma is_conformal_map_complex_linear {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
+  is_conformal_map (map.restrict_scalars ℝ) :=
 begin
   have minor₁ : ∥map 1∥ ≠ 0,
   { simpa [ext_ring_iff] using nonzero },
@@ -56,8 +56,7 @@ begin
     simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm],
     field_simp [minor₁], },
   { ext1,
-    rw [← linear_isometry.coe_to_linear_map],
-    simp [minor₁], },
+    simp [minor₁] },
 end
 
 lemma is_conformal_map_complex_linear_conj
@@ -77,23 +76,21 @@ lemma is_conformal_map.is_complex_or_conj_linear (h : is_conformal_map g) :
   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g) ∨
   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g ∘L ↑conj_cle) :=
 begin
-  rcases h with ⟨c, hc, li, hg⟩,
-  rcases linear_isometry_complex (li.to_linear_isometry_equiv rfl) with ⟨a, ha⟩,
-  let rot := c • (a : ℂ) • continuous_linear_map.id ℂ ℂ,
-  cases ha,
-  { refine or.intro_left _ ⟨rot, _⟩,
+  rcases h with ⟨c, hc, li, rfl⟩,
+  obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.to_linear_isometry = li,
+    from ⟨li.to_linear_isometry_equiv rfl, by { ext1, refl }⟩,
+  rcases linear_isometry_complex li with ⟨a, rfl|rfl⟩,
+  -- let rot := c • (a : ℂ) • continuous_linear_map.id ℂ ℂ,
+  { refine or.inl ⟨c • (a : ℂ) • continuous_linear_map.id ℂ ℂ, _⟩,
     ext1,
-    simp only [coe_restrict_scalars', hg, ← li.coe_to_linear_isometry_equiv, ha,
-               pi.smul_apply, continuous_linear_map.smul_apply, rotation_apply,
-               continuous_linear_map.id_apply, smul_eq_mul], },
-  { refine or.intro_right _ ⟨rot, _⟩,
+    simp only [coe_restrict_scalars', smul_apply, linear_isometry.coe_to_continuous_linear_map,
+      linear_isometry_equiv.coe_to_linear_isometry, rotation_apply, id_apply, smul_eq_mul] },
+  { refine or.inr ⟨c • (a : ℂ) • continuous_linear_map.id ℂ ℂ, _⟩,
     ext1,
-    rw [continuous_linear_map.coe_comp', hg, ← li.coe_to_linear_isometry_equiv, ha],
-    simp only [coe_restrict_scalars', function.comp_app, pi.smul_apply,
-               linear_isometry_equiv.coe_trans, conj_lie_apply,
-               rotation_apply, continuous_linear_equiv.coe_apply, conj_cle_apply],
-    simp only [continuous_linear_map.smul_apply, continuous_linear_map.id_apply,
-               smul_eq_mul, conj_conj], },
+    simp only [coe_restrict_scalars', smul_apply, linear_isometry.coe_to_continuous_linear_map,
+      linear_isometry_equiv.coe_to_linear_isometry, rotation_apply, id_apply, smul_eq_mul,
+      comp_apply, linear_isometry_equiv.trans_apply, continuous_linear_equiv.coe_coe,
+      conj_cle_apply, conj_lie_apply, conj_conj] },
 end
 
 /-- A real continuous linear map on the complex plane is conformal if and only if the map or its

src/analysis/complex/real_deriv.lean

@@ -122,20 +122,17 @@ section conformality
 open complex continuous_linear_map
 open_locale complex_conjugate
 
+variables {E : Type*} [normed_group E] [normed_space ℂ E] {z : ℂ} {f : ℂ → E}
+
 /-- A real differentiable function of the complex plane into some complex normed space `E` is
     conformal at a point `z` if it is holomorphic at that point with a nonvanishing differential.
     This is a version of the Cauchy-Riemann equations. -/
-lemma differentiable_at.conformal_at {E : Type*}
-  [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
-  {z : ℂ} {f : ℂ → E}
-  (hf' : fderiv ℝ f z ≠ 0) (h : differentiable_at ℂ f z) :
+lemma differentiable_at.conformal_at (h : differentiable_at ℂ f z) (hf' : deriv f z ≠ 0) :
   conformal_at f z :=
 begin
-  rw conformal_at_iff_is_conformal_map_fderiv,
-  rw (h.has_fderiv_at.restrict_scalars ℝ).fderiv at ⊢ hf',
+  rw [conformal_at_iff_is_conformal_map_fderiv, (h.has_fderiv_at.restrict_scalars ℝ).fderiv],
   apply is_conformal_map_complex_linear,
-  contrapose! hf' with w,
-  simp [w]
+  simpa only [ne.def, ext_ring_iff]
 end
 
 /-- A complex function is conformal if and only if the function is holomorphic or antiholomorphic

src/analysis/inner_product_space/conformal_linear_map.lean

@@ -17,27 +17,23 @@ variables {E F : Type*} [inner_product_space ℝ E] [inner_product_space ℝ F]
 open linear_isometry continuous_linear_map
 open_locale real_inner_product_space
 
-lemma is_conformal_map_iff (f' : E →L[ℝ] F) :
-  is_conformal_map f' ↔ ∃ (c : ℝ), 0 < c ∧
-  ∀ (u v : E), ⟪f' u, f' v⟫ = (c : ℝ) * ⟪u, v⟫ :=
+/-- A map between two inner product spaces is a conformal map if and only if it preserves inner
+products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that `⟪f u, f v⟫ = c *
+⟪u, v⟫` for all `u`, `v`. -/
+lemma is_conformal_map_iff (f : E →L[ℝ] F) :
+  is_conformal_map f ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), ⟪f u, f v⟫ = c * ⟪u, v⟫ :=
 begin
   split,
-  { rintros ⟨c₁, hc₁, li, h⟩,
+  { rintros ⟨c₁, hc₁, li, rfl⟩,
     refine ⟨c₁ * c₁, mul_self_pos.2 hc₁, λ u v, _⟩,
-    simp only [h, pi.smul_apply, inner_map_map,
-               real_inner_smul_left, real_inner_smul_right, mul_assoc], },
+    simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul',
+      coe_to_continuous_linear_map, pi.smul_apply, inner_map_map] },
   { rintros ⟨c₁, hc₁, huv⟩,
-    let c := real.sqrt c₁⁻¹,
-    have hc : c ≠ 0 := λ w, by {simp only [c] at w;
-      exact (real.sqrt_ne_zero'.mpr $ inv_pos.mpr hc₁) w},
-    let f₁ := c • f',
-    have minor : (f₁ : E → F) = c • f' := rfl,
-    have minor' : (f' : E → F) = c⁻¹ • f₁ := by ext;
-      simp_rw [minor, pi.smul_apply]; rw [smul_smul, inv_mul_cancel hc, one_smul],
-    refine ⟨c⁻¹, inv_ne_zero hc, f₁.to_linear_map.isometry_of_inner (λ u v, _), minor'⟩,
-    simp_rw [to_linear_map_eq_coe, continuous_linear_map.coe_coe, minor, pi.smul_apply],
-    rw [real_inner_smul_left, real_inner_smul_right,
-        huv u v, ← mul_assoc, ← mul_assoc,
-        real.mul_self_sqrt $ le_of_lt $ inv_pos.mpr hc₁,
-        inv_mul_cancel $ ne_of_gt hc₁, one_mul], },
+    obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c,
+      from ⟨real.sqrt c₁, real.sqrt_pos.2 hc₁, (real.mul_self_sqrt hc₁.le).symm⟩,
+    refine ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometry_of_inner (λ u v, _), _⟩,
+    { simp only [real_inner_smul_left, real_inner_smul_right, huv, mul_assoc, coe_smul,
+        inv_mul_cancel_left₀ hc.ne', linear_map.smul_apply, continuous_linear_map.coe_coe] },
+    { ext1 x,
+      exact (smul_inv_smul₀ hc.ne' (f x)).symm } }
 end

src/analysis/normed_space/conformal_linear_map.lean

@@ -40,66 +40,63 @@ The definition of conformality in this file does NOT require the maps to be orie
 
 noncomputable theory
 
-open linear_isometry continuous_linear_map
+open function linear_isometry continuous_linear_map
 
 /-- A continuous linear map `f'` is said to be conformal if it's
     a nonzero multiple of a linear isometry. -/
 def is_conformal_map {R : Type*} {X Y : Type*} [normed_field R]
   [semi_normed_group X] [semi_normed_group Y] [normed_space R X] [normed_space R Y]
   (f' : X →L[R] Y) :=
-∃ (c : R) (hc : c ≠ 0) (li : X →ₗᵢ[R] Y), (f' : X → Y) = c • li
+∃ (c : R) (hc : c ≠ 0) (li : X →ₗᵢ[R] Y), f' = c • li.to_continuous_linear_map
 
 variables {R M N G M' : Type*} [normed_field R]
   [semi_normed_group M] [semi_normed_group N] [semi_normed_group G]
   [normed_space R M] [normed_space R N] [normed_space R G]
   [normed_group M'] [normed_space R M']
+  {f : M →L[R] N} {g : N →L[R] G} {c : R}
 
 lemma is_conformal_map_id : is_conformal_map (id R M) :=
-⟨1, one_ne_zero, id, by { ext, simp }⟩
+⟨1, one_ne_zero, id, by simp⟩
 
-lemma is_conformal_map_const_smul {c : R} (hc : c ≠ 0) : is_conformal_map (c • (id R M)) :=
-⟨c, hc, id, by { ext, simp }⟩
+lemma is_conformal_map.smul (hf : is_conformal_map f) {c : R} (hc : c ≠ 0) :
+  is_conformal_map (c • f) :=
+begin
+  rcases hf with ⟨c', hc', li, rfl⟩,
+  exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩
+end
+
+lemma is_conformal_map_const_smul (hc : c ≠ 0) : is_conformal_map (c • id R M) :=
+is_conformal_map_id.smul hc
 
-lemma linear_isometry.is_conformal_map (f' : M →ₗᵢ[R] N) :
+protected lemma linear_isometry.is_conformal_map (f' : M →ₗᵢ[R] N) :
   is_conformal_map f'.to_continuous_linear_map :=
-⟨1, one_ne_zero, f', by { ext, simp }⟩
+⟨1, one_ne_zero, f', (one_smul _ _).symm⟩
 
-lemma is_conformal_map_of_subsingleton [h : subsingleton M] (f' : M →L[R] N) :
+@[nontriviality] lemma is_conformal_map_of_subsingleton [subsingleton M] (f' : M →L[R] N) :
   is_conformal_map f' :=
-begin
-  rw subsingleton_iff at h,
-  have minor : (f' : M → N) = function.const M 0 := by ext x'; rw h x' 0; exact f'.map_zero,
-  have key : ∀ (x' : M), ∥(0 : M →ₗ[R] N) x'∥ = ∥x'∥ := λ x',
-    by { rw [linear_map.zero_apply, h x' 0], repeat { rw norm_zero }, },
-  exact ⟨(1 : R), one_ne_zero, ⟨0, key⟩,
-    by { rw pi.smul_def, ext p, rw [one_smul, minor], refl, }⟩,
-end
+⟨1, one_ne_zero, ⟨0, λ x, by simp [subsingleton.elim x 0]⟩, subsingleton.elim _ _⟩
 
 namespace is_conformal_map
 
-lemma comp {f' : M →L[R] N} {g' : N →L[R] G}
-  (hg' : is_conformal_map g') (hf' : is_conformal_map f') :
-  is_conformal_map (g'.comp f') :=
+lemma comp (hg : is_conformal_map g) (hf : is_conformal_map f) :
+  is_conformal_map (g.comp f) :=
 begin
-  rcases hf' with ⟨cf, hcf, lif, hlif⟩,
-  rcases hg' with ⟨cg, hcg, lig, hlig⟩,
-  refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, funext (λ x, _)⟩,
-  simp only [coe_comp', linear_isometry.coe_comp, hlif, hlig, pi.smul_apply,
-             function.comp_app, linear_isometry.map_smul, smul_smul],
+  rcases hf with ⟨cf, hcf, lif, rfl⟩,
+  rcases hg with ⟨cg, hcg, lig, rfl⟩,
+  refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, _⟩,
+  rw [smul_comp, comp_smul, mul_smul],
+  refl
 end
 
-lemma injective {f' : M' →L[R] N} (h : is_conformal_map f') : function.injective f' :=
-let ⟨c, hc, li, hf'⟩ := h in by simp only [hf', pi.smul_def];
-  exact (smul_right_injective _ hc).comp li.injective
+protected lemma injective {f : M' →L[R] N} (h : is_conformal_map f) : function.injective f :=
+by { rcases h with ⟨c, hc, li, rfl⟩, exact (smul_right_injective _ hc).comp li.injective }
 
 lemma ne_zero [nontrivial M'] {f' : M' →L[R] N} (hf' : is_conformal_map f') :
   f' ≠ 0 :=
 begin
-  intros w,
+  rintro rfl,
   rcases exists_ne (0 : M') with ⟨a, ha⟩,
-  have : f' a = f' 0,
-  { simp_rw [w, continuous_linear_map.zero_apply], },
-  exact ha (hf'.injective this),
+  exact ha (hf'.injective rfl)
 end
 
 end is_conformal_map

src/analysis/normed_space/linear_isometry.lean

@@ -74,6 +74,8 @@ instance : has_coe_to_fun (E →ₛₗᵢ[σ₁₂] E₂) (λ _, E → E₂) :=
 
 @[simp] lemma coe_to_linear_map : ⇑f.to_linear_map = f := rfl
 
+@[simp] lemma coe_mk (f : E →ₛₗ[σ₁₂] E₂) (hf) : ⇑(mk f hf) = f := rfl
+
 lemma coe_injective : @injective (E →ₛₗᵢ[σ₁₂] E₂) (E → E₂) coe_fn :=
 fun_like.coe_injective
 
@@ -169,6 +171,9 @@ def id : E →ₗᵢ[R] E := ⟨linear_map.id, λ x, rfl⟩
 
 @[simp] lemma id_to_linear_map : (id.to_linear_map : E →ₗ[R] E) = linear_map.id := rfl
 
+@[simp] lemma id_to_continuous_linear_map :
+  id.to_continuous_linear_map = continuous_linear_map.id R E := rfl
+
 instance : inhabited (E →ₗᵢ[R] E) := ⟨id⟩
 
 /-- Composition of linear isometries. -/