feat(analysis/inner_product_space/pi_L2): map_isometry_euclidean_of_orthonormal (#11907)

Add a lemma giving the result of `isometry_euclidean_of_orthonormal`
when applied to an orthonormal basis obtained from another orthonormal
basis with `basis.map`.

Author: jsm28

src/analysis/inner_product_space/pi_L2.lean

@@ -38,6 +38,7 @@ noncomputable theory
 
 variables {ι : Type*}
 variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [inner_product_space 𝕜 E]
+variables {E' : Type*} [inner_product_space 𝕜 E']
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
 /-
@@ -176,6 +177,16 @@ rfl
   ((v.isometry_euclidean_of_orthonormal hv).symm : euclidean_space 𝕜 ι → E) = v.equiv_fun.symm :=
 rfl
 
+/-- 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).isometry_euclidean_of_orthonormal (hv.map_linear_isometry_equiv f) =
+    f.symm.trans (v.isometry_euclidean_of_orthonormal hv) :=
+linear_isometry_equiv.to_linear_equiv_injective $ v.map_equiv_fun _
+
 end
 
 /-- `ℂ` is isometric to `ℝ²` with the Euclidean inner product. -/