English
The coordinate projection induced by transforming a basis to an orthonormal basis matches the original coordinate representation.
Русский
Координатное отображение, полученное из преобразования базиса в ортонормированный базис, совпадает с исходным представлением координат.
LaTeX
$$$((v.toOrthonormalBasis hv).repr : E → EuclideanSpace 𝕜 ι) = v.equivFun$$$
Lean4
/-- A basis that is orthonormal is an orthonormal basis. -/
def _root_.Module.Basis.toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) : OrthonormalBasis ι 𝕜 E :=
OrthonormalBasis.ofRepr <|
LinearEquiv.isometryOfInner v.equivFun
(by
intro x y
let p : EuclideanSpace 𝕜 ι := v.equivFun x
let q : EuclideanSpace 𝕜 ι := v.equivFun y
have key : ⟪p, q⟫ = ⟪∑ i, p i • v i, ∑ i, q i • v i⟫ := by
simp [inner_sum, inner_smul_right, hv.inner_left_fintype, PiLp.inner_apply]
convert key
· rw [← v.equivFun.symm_apply_apply x, v.equivFun_symm_apply]
· rw [← v.equivFun.symm_apply_apply y, v.equivFun_symm_apply])
