Commit 2022-10-12 10:35 265fe3d8

View on Github →

feat(analysis/inner_product_space/orientation): volume form (#16487) Construct the volume form, a uniquely-determined top-dimensional alternating form on an oriented real inner product space. Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/analysis/inner_product_space/orientation.lean

added theorem orientation.abs_volume_form_apply_le

added theorem orientation.abs_volume_form_apply_of_orthonormal

added theorem orientation.abs_volume_form_apply_of_pairwise_orthogonal

modified theorem orientation.fin_orthonormal_basis_orientation

added def orientation.volume_form

added theorem orientation.volume_form_apply_le

added theorem orientation.volume_form_robust'

added theorem orientation.volume_form_robust

added theorem orientation.volume_form_zero_neg

added theorem orientation.volume_form_zero_pos

added theorem orthonormal_basis.abs_det_adjust_to_orientation

modified def orthonormal_basis.adjust_to_orientation

modified theorem orthonormal_basis.adjust_to_orientation_apply_eq_or_eq_neg

added theorem orthonormal_basis.det_adjust_to_orientation

added theorem orthonormal_basis.det_to_matrix_orthonormal_basis_of_same_orientation

modified theorem orthonormal_basis.orientation_adjust_to_orientation

modified theorem orthonormal_basis.orthonormal_adjust_to_orientation

added theorem orthonormal_basis.same_orientation_iff_det_eq_det

modified theorem orthonormal_basis.to_basis_adjust_to_orientation

Modified src/linear_algebra/determinant.lean

added theorem basis.det_is_empty

Modified src/linear_algebra/orientation.lean

added theorem basis.orientation_is_empty

added theorem orientation.eq_or_eq_neg_of_is_empty