English
The volume form is invariant under positively oriented isometric automorphisms of E: pulling back by φ preserves volume form.
Русский
Объемная форма сохраняется при применении к положительно ориентированным изометрическим аутоморфизмам пространства.
LaTeX
$$$$ o.volumeForm(\phi \circ x) = o.volumeForm(x) $$ for any positively oriented isometry \phi.$$
Lean4
theorem volumeForm_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (finrank ℝ F = n)]
(φ : E ≃ₗᵢ[ℝ] F) (x : Fin n → F) :
(Orientation.map (Fin n) φ.toLinearEquiv o).volumeForm x = o.volumeForm (φ.symm ∘ x) :=
by
rcases n with - | n
· refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
have he : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation n.succ_pos Fact.out
have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o :=
by
rw [← he]
exact e.toBasis.orientation_map φ.toLinearEquiv
rw [(Orientation.map (Fin n.succ) φ.toLinearEquiv o).volumeForm_robust (e.map φ) heφ]
rw [o.volumeForm_robust e he]
simp
