English
If the orientation relative to a basis is opposite, the volume form equals the negative determinant: the sign flips with opposite orientation.
Русский
Если ориентация противоречит базису, объемная форма равна минусу детерминанта; знак меняется при противоположной ориентации.
LaTeX
$$$$ o.volumeForm = -\, b.toBasis.det \quad\text{when } b.toBasis.orientation \neq 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_neg (b : OrthonormalBasis (Fin n) ℝ E) (hb : b.toBasis.orientation ≠ o) :
o.volumeForm = -b.toBasis.det := by
rcases n with - | n
·
classical
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Nat.rec_zero, Basis.det_isEmpty]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
simp_rw [volumeForm]
apply e.det_eq_neg_det_of_opposite_orientation b
convert hb.symm
exact o.finOrthonormalBasis_orientation _ _
