English
The volume form can be computed as the determinant with respect to any orthonormal basis whose orientation agrees with the given orientation; i.e., the volume form equals the determinant in that basis.
Русский
Объемная форма может быть вычислена как детерминант по любому ортонормированному базису, чья ориентация согласуется с данной ориентацией; то есть объемная форма равна детерминанту в этом базисе.
LaTeX
$$$$ o.volumeForm = b.toBasis.det \quad\text{whenever } b.toBasis.orientation = o. $$$$
Lean4
/-- The volume form on an oriented real inner product space can be evaluated as the determinant with
respect to any orthonormal basis of the space compatible with the orientation. -/
theorem volumeForm_robust (b : OrthonormalBasis (Fin n) ℝ E) (hb : b.toBasis.orientation = o) :
o.volumeForm = b.toBasis.det := by
cases n
·
classical
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
simp_rw [volumeForm, Or.by_cases, dif_pos this, Nat.rec_zero, Basis.det_isEmpty]
· simp_rw [volumeForm]
rw [same_orientation_iff_det_eq_det, hb]
exact o.finOrthonormalBasis_orientation _ _
