feat(analysis/inner_product/orientation, geometry/euclidean/oriented_…

…angle): use bundled orthonormal bases (#16475)

Bundled orthonormal bases (as opposed to bases with a mixin predicate `orthonormal`) were defined in #12060, and some of the use cases were switched over in #12253. This PR completes the job, switching to bundled orthonormal bases in `inner_product/orientation` and `euclidean/oriented_angle` as well as in one remaining construction (the standard ` ℝ`-orthonormal basis of `ℂ`) in `inner_product/pi_L2`.

Formalized as part of the Sphere Eversion project.  The part that I will be using in future PRs is the bundled version of the construction `orthonormal_basis.adjust_to_orientation` in `inner_product/orientation`.

src/analysis/inner_product_space/orientation.lean

@@ -21,42 +21,64 @@ orientation.
 noncomputable theory
 
 variables {E : Type*} [inner_product_space ℝ E]
-variables {ι : Type*} [fintype ι] [decidable_eq ι]
 
 open finite_dimensional
 
-/-- `basis.adjust_to_orientation`, applied to an orthonormal basis, produces an orthonormal
-basis. -/
-lemma orthonormal.orthonormal_adjust_to_orientation [nonempty ι] {e : basis ι ℝ E}
-  (h : orthonormal ℝ e) (x : orientation ℝ E ι) : orthonormal ℝ (e.adjust_to_orientation x) :=
-h.orthonormal_of_forall_eq_or_eq_neg (e.adjust_to_orientation_apply_eq_or_eq_neg x)
+section adjust_to_orientation
+variables {ι : Type*} [fintype ι] [decidable_eq ι] [nonempty ι] (e : orthonormal_basis ι ℝ E)
+  (x : orientation ℝ E ι)
 
-/-- An orthonormal basis, indexed by `fin n`, with the given orientation. -/
-protected def orientation.fin_orthonormal_basis {n : ℕ} (hn : 0 < n) (h : finrank ℝ E = n)
-  (x : orientation ℝ E (fin n)) : basis (fin n) ℝ E :=
+/-- `orthonormal_basis.adjust_to_orientation`, applied to an orthonormal basis, produces an
+orthonormal basis. -/
+lemma orthonormal_basis.orthonormal_adjust_to_orientation :
+  orthonormal ℝ (e.to_basis.adjust_to_orientation x) :=
 begin
-  haveI := fin.pos_iff_nonempty.1 hn,
-  haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
-  exact (fin_std_orthonormal_basis h).to_basis.adjust_to_orientation x
+  apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg,
+  simpa using e.to_basis.adjust_to_orientation_apply_eq_or_eq_neg x
 end
 
-/-- `orientation.fin_orthonormal_basis` is orthonormal. -/
-protected lemma orientation.fin_orthonormal_basis_orthonormal {n : ℕ} (hn : 0 < n)
-  (h : finrank ℝ E = n) (x : orientation ℝ E (fin n)) :
-  orthonormal ℝ (x.fin_orthonormal_basis hn h) :=
+/-- Given an orthonormal basis and an orientation, return an orthonormal basis giving that
+orientation: either the original basis, or one constructed by negating a single (arbitrary) basis
+vector. -/
+def orthonormal_basis.adjust_to_orientation : orthonormal_basis ι ℝ E :=
+(e.to_basis.adjust_to_orientation x).to_orthonormal_basis (e.orthonormal_adjust_to_orientation x)
+
+lemma orthonormal_basis.to_basis_adjust_to_orientation :
+  (e.adjust_to_orientation x).to_basis = e.to_basis.adjust_to_orientation x :=
+(e.to_basis.adjust_to_orientation x).to_basis_to_orthonormal_basis _
+
+/-- `adjust_to_orientation` gives an orthonormal basis with the required orientation. -/
+@[simp] lemma orthonormal_basis.orientation_adjust_to_orientation :
+  (e.adjust_to_orientation x).to_basis.orientation = x :=
+begin
+  rw e.to_basis_adjust_to_orientation,
+  exact e.to_basis.orientation_adjust_to_orientation x,
+end
+
+/-- Every basis vector from `adjust_to_orientation` is either that from the original basis or its
+negation. -/
+lemma orthonormal_basis.adjust_to_orientation_apply_eq_or_eq_neg (i : ι) :
+  e.adjust_to_orientation x i = e i ∨ e.adjust_to_orientation x i = -(e i) :=
+by simpa [← e.to_basis_adjust_to_orientation]
+  using e.to_basis.adjust_to_orientation_apply_eq_or_eq_neg x i
+
+end adjust_to_orientation
+
+/-- An orthonormal basis, indexed by `fin n`, with the given orientation. -/
+protected def orientation.fin_orthonormal_basis {n : ℕ} (hn : 0 < n) (h : finrank ℝ E = n)
+  (x : orientation ℝ E (fin n)) : orthonormal_basis (fin n) ℝ E :=
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
   haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
-  exact (show orthonormal ℝ (fin_std_orthonormal_basis h).to_basis, -- Note sure how to format this
-    by simp only [orthonormal_basis.coe_to_basis, orthonormal_basis.orthonormal]
-    ).orthonormal_adjust_to_orientation _
+  exact (fin_std_orthonormal_basis h).adjust_to_orientation x
 end
 
 /-- `orientation.fin_orthonormal_basis` gives a basis with the required orientation. -/
 @[simp] lemma orientation.fin_orthonormal_basis_orientation {n : ℕ} (hn : 0 < n)
   (h : finrank ℝ E = n) (x : orientation ℝ E (fin n)) :
-  (x.fin_orthonormal_basis hn h).orientation = x :=
+  (x.fin_orthonormal_basis hn h).to_basis.orientation = x :=
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
-  exact basis.orientation_adjust_to_orientation _ _
+  haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
+  exact (fin_std_orthonormal_basis h).orientation_adjust_to_orientation x
 end

src/analysis/inner_product_space/pi_L2.lean

@@ -348,6 +348,11 @@ protected def map {G : Type*} [inner_product_space 𝕜 G] (b : orthonormal_basi
   (b : orthonormal_basis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) :
   b.map L i = L (b i) := rfl
 
+@[simp] protected lemma to_basis_map {G : Type*} [inner_product_space 𝕜 G]
+  (b : orthonormal_basis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :
+  (b.map L).to_basis = b.to_basis.map L.to_linear_equiv :=
+rfl
+
 /-- A basis that is orthonormal is an orthonormal basis. -/
 def _root_.basis.to_orthonormal_basis (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
   orthonormal_basis ι 𝕜 E :=
@@ -470,66 +475,52 @@ by { classical,
 
 end orthonormal_basis
 
-/-- If `f : E ≃ₗᵢ[𝕜] E'` is a linear isometry of inner product spaces then an orthonormal basis `v`
-of `E` determines a linear isometry `e : E' ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι`. This result states that
-`e` may be obtained either by transporting `v` to `E'` or by composing with the linear isometry
-`E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι` provided by `v`. -/
-@[simp] lemma basis.map_isometry_euclidean_of_orthonormal (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v)
-  (f : E ≃ₗᵢ[𝕜] E') :
-  ((v.map f.to_linear_equiv).to_orthonormal_basis (hv.map_linear_isometry_equiv f)).repr =
-    f.symm.trans (v.to_orthonormal_basis hv).repr :=
-linear_isometry_equiv.to_linear_equiv_injective $ v.map_equiv_fun _
-
-/-- `ℂ` is isometric to `ℝ²` with the Euclidean inner product. -/
-def complex.isometry_euclidean : ℂ ≃ₗᵢ[ℝ] (euclidean_space ℝ (fin 2)) :=
+/-- `![1, I]` is an orthonormal basis for `ℂ` considered as a real inner product space. -/
+def complex.orthonormal_basis_one_I : orthonormal_basis (fin 2) ℝ ℂ :=
 (complex.basis_one_I.to_orthonormal_basis
 begin
   rw orthonormal_iff_ite,
   intros i, fin_cases i;
   intros j; fin_cases j;
   simp [real_inner_eq_re_inner]
-end).repr
+end)
 
-@[simp] lemma complex.isometry_euclidean_symm_apply (x : euclidean_space ℝ (fin 2)) :
-  complex.isometry_euclidean.symm x = (x 0) + (x 1) * I :=
-begin
-  convert complex.basis_one_I.equiv_fun_symm_apply x,
-  { simpa },
-  { simp },
-end
+@[simp] lemma complex.orthonormal_basis_one_I_repr_apply (z : ℂ) :
+  complex.orthonormal_basis_one_I.repr z =  ![z.re, z.im] :=
+rfl
 
-lemma complex.isometry_euclidean_proj_eq_self (z : ℂ) :
-  ↑(complex.isometry_euclidean z 0) + ↑(complex.isometry_euclidean z 1) * (I : ℂ) = z :=
-by rw [← complex.isometry_euclidean_symm_apply (complex.isometry_euclidean z),
-  complex.isometry_euclidean.symm_apply_apply z]
+@[simp] lemma complex.orthonormal_basis_one_I_repr_symm_apply (x : euclidean_space ℝ (fin 2)) :
+  complex.orthonormal_basis_one_I.repr.symm x = (x 0) + (x 1) * I :=
+rfl
 
-@[simp] lemma complex.isometry_euclidean_apply_zero (z : ℂ) :
-  complex.isometry_euclidean z 0 = z.re :=
-by { conv_rhs { rw ← complex.isometry_euclidean_proj_eq_self z }, simp }
+@[simp] lemma complex.to_basis_orthonormal_basis_one_I :
+  complex.orthonormal_basis_one_I.to_basis = complex.basis_one_I :=
+basis.to_basis_to_orthonormal_basis _ _
 
-@[simp] lemma complex.isometry_euclidean_apply_one (z : ℂ) :
-  complex.isometry_euclidean z 1 = z.im :=
-by { conv_rhs { rw ← complex.isometry_euclidean_proj_eq_self z }, simp }
+@[simp] lemma complex.coe_orthonormal_basis_one_I :
+  (complex.orthonormal_basis_one_I : (fin 2) → ℂ) = ![1, I] :=
+by simp [complex.orthonormal_basis_one_I]
 
 /-- The isometry between `ℂ` and a two-dimensional real inner product space given by a basis. -/
-def complex.isometry_of_orthonormal {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v) : ℂ ≃ₗᵢ[ℝ] F :=
-complex.isometry_euclidean.trans (v.to_orthonormal_basis hv).repr.symm
+def complex.isometry_of_orthonormal (v : orthonormal_basis (fin 2) ℝ F) : ℂ ≃ₗᵢ[ℝ] F :=
+complex.orthonormal_basis_one_I.repr.trans v.repr.symm
 
-@[simp] lemma complex.map_isometry_of_orthonormal {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v)
+@[simp] lemma complex.map_isometry_of_orthonormal (v : orthonormal_basis (fin 2) ℝ F)
   (f : F ≃ₗᵢ[ℝ] F') :
-  complex.isometry_of_orthonormal (hv.map_linear_isometry_equiv f) =
-    (complex.isometry_of_orthonormal hv).trans f :=
-by simp [complex.isometry_of_orthonormal, linear_isometry_equiv.trans_assoc]
+  complex.isometry_of_orthonormal (v.map f) =
+    (complex.isometry_of_orthonormal v).trans f :=
+by simp [complex.isometry_of_orthonormal, linear_isometry_equiv.trans_assoc, orthonormal_basis.map]
 
 lemma complex.isometry_of_orthonormal_symm_apply
-  {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v) (f : F) :
-  (complex.isometry_of_orthonormal hv).symm f = (v.coord 0 f : ℂ) + (v.coord 1 f : ℂ) * I :=
+  (v : orthonormal_basis (fin 2) ℝ F) (f : F) :
+  (complex.isometry_of_orthonormal v).symm f
+  = (v.to_basis.coord 0 f : ℂ) + (v.to_basis.coord 1 f : ℂ) * I :=
 by simp [complex.isometry_of_orthonormal]
 
 lemma complex.isometry_of_orthonormal_apply
-  {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ v) (z : ℂ) :
-  complex.isometry_of_orthonormal hv z = z.re • v 0 + z.im • v 1 :=
-by simp [complex.isometry_of_orthonormal, (dec_trivial : (finset.univ : finset (fin 2)) = {0, 1})]
+  (v : orthonormal_basis (fin 2) ℝ F) (z : ℂ) :
+  complex.isometry_of_orthonormal v z = z.re • v 0 + z.im • v 1 :=
+by simp [complex.isometry_of_orthonormal, ← v.sum_repr_symm]
 
 open finite_dimensional