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.

src/analysis/inner_product_space/orientation.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2022 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Myers
+Authors: Joseph Myers, Heather Macbeth
 -/
-import analysis.inner_product_space.pi_L2
+import analysis.inner_product_space.gram_schmidt_ortho
 import linear_algebra.orientation
 
 /-!
@@ -13,8 +13,23 @@ This file provides definitions and proves lemmas about orientations of real inne
 
 ## Main definitions
 
+* `orthonormal_basis.adjust_to_orientation` takes an orthonormal basis and an orientation, and
+  returns an orthonormal basis with that orientation: either the original orthonormal basis, or one
+  constructed by negating a single (arbitrary) basis vector.
 * `orientation.fin_orthonormal_basis` is an orthonormal basis, indexed by `fin n`, with the given
-orientation.
+  orientation.
+* `orientation.volume_form` is a nonvanishing top-dimensional alternating form on an oriented real
+  inner product space, uniquely defined by compatibility with the orientation and inner product
+  structure.
+
+## Main theorems
+
+* `orientation.volume_form_apply_le` states that the result of applying the volume form to a set of
+  `n` vectors, where `n` is the dimension the inner product space, is bounded by the product of the
+  lengths of the vectors.
+* `orientation.abs_volume_form_apply_of_pairwise_orthogonal` states that the result of applying the
+  volume form to a set of `n` orthogonal vectors, where `n` is the dimension the inner product
+  space, is equal up to sign to the product of the lengths of the vectors.
 
 -/
 
@@ -23,15 +38,49 @@ noncomputable theory
 variables {E : Type*} [inner_product_space ℝ E]
 
 open finite_dimensional
+open_locale big_operators real_inner_product_space
 
-section adjust_to_orientation
-variables {ι : Type*} [fintype ι] [decidable_eq ι] [nonempty ι] (e : orthonormal_basis ι ℝ E)
+namespace orthonormal_basis
+variables {ι : Type*} [fintype ι] [decidable_eq ι] [ne : nonempty ι] (e f : orthonormal_basis ι ℝ E)
   (x : orientation ℝ E ι)
 
-/-- `orthonormal_basis.adjust_to_orientation`, applied to an orthonormal basis, produces an
-orthonormal basis. -/
-lemma orthonormal_basis.orthonormal_adjust_to_orientation :
-  orthonormal ℝ (e.to_basis.adjust_to_orientation x) :=
+/-- The change-of-basis matrix between two orthonormal bases with the same orientation has
+determinant 1. -/
+lemma det_to_matrix_orthonormal_basis_of_same_orientation
+  (h : e.to_basis.orientation = f.to_basis.orientation) :
+  e.to_basis.det f = 1 :=
+begin
+  apply (e.det_to_matrix_orthonormal_basis_real f).resolve_right,
+  have : 0 < e.to_basis.det f,
+  { rw e.to_basis.orientation_eq_iff_det_pos at h,
+    simpa using h },
+  linarith,
+end
+
+variables {e f}
+
+/-- Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional
+form on `E`, and conversely. -/
+lemma same_orientation_iff_det_eq_det :
+  e.to_basis.det = f.to_basis.det ↔ e.to_basis.orientation = f.to_basis.orientation :=
+begin
+  split,
+  { intros h,
+    dsimp [basis.orientation],
+    congr' },
+  { intros h,
+    rw e.to_basis.det.eq_smul_basis_det f.to_basis,
+    simp [e.det_to_matrix_orthonormal_basis_of_same_orientation f h], },
+end
+
+variables (e)
+
+section adjust_to_orientation
+include ne
+
+/-- `orthonormal_basis.adjust_to_orientation`, applied to an orthonormal basis, preserves the
+property of orthonormality. -/
+lemma orthonormal_adjust_to_orientation : orthonormal ℝ (e.to_basis.adjust_to_orientation x) :=
 begin
   apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg,
   simpa using e.to_basis.adjust_to_orientation_apply_eq_or_eq_neg x
@@ -40,15 +89,15 @@ end
 /-- Given an orthonormal basis and an orientation, return an orthonormal basis giving that
 orientation: either the original basis, or one constructed by negating a single (arbitrary) basis
 vector. -/
-def orthonormal_basis.adjust_to_orientation : orthonormal_basis ι ℝ E :=
+def adjust_to_orientation : orthonormal_basis ι ℝ E :=
 (e.to_basis.adjust_to_orientation x).to_orthonormal_basis (e.orthonormal_adjust_to_orientation x)
 
-lemma orthonormal_basis.to_basis_adjust_to_orientation :
+lemma to_basis_adjust_to_orientation :
   (e.adjust_to_orientation x).to_basis = e.to_basis.adjust_to_orientation x :=
 (e.to_basis.adjust_to_orientation x).to_basis_to_orthonormal_basis _
 
 /-- `adjust_to_orientation` gives an orthonormal basis with the required orientation. -/
-@[simp] lemma orthonormal_basis.orientation_adjust_to_orientation :
+@[simp] lemma orientation_adjust_to_orientation :
   (e.adjust_to_orientation x).to_basis.orientation = x :=
 begin
   rw e.to_basis_adjust_to_orientation,
@@ -57,15 +106,31 @@ end
 
 /-- Every basis vector from `adjust_to_orientation` is either that from the original basis or its
 negation. -/
-lemma orthonormal_basis.adjust_to_orientation_apply_eq_or_eq_neg (i : ι) :
+lemma adjust_to_orientation_apply_eq_or_eq_neg (i : ι) :
   e.adjust_to_orientation x i = e i ∨ e.adjust_to_orientation x i = -(e i) :=
 by simpa [← e.to_basis_adjust_to_orientation]
   using e.to_basis.adjust_to_orientation_apply_eq_or_eq_neg x i
 
+lemma det_adjust_to_orientation :
+  (e.adjust_to_orientation x).to_basis.det = e.to_basis.det
+  ∨ (e.adjust_to_orientation x).to_basis.det = -e.to_basis.det :=
+by simpa using e.to_basis.det_adjust_to_orientation x
+
+lemma abs_det_adjust_to_orientation (v : ι → E) :
+  |(e.adjust_to_orientation x).to_basis.det v| = |e.to_basis.det v| :=
+by simp [to_basis_adjust_to_orientation]
+
 end adjust_to_orientation
 
+end orthonormal_basis
+
+namespace orientation
+variables {n : ℕ}
+
+open orthonormal_basis
+
 /-- An orthonormal basis, indexed by `fin n`, with the given orientation. -/
-protected def orientation.fin_orthonormal_basis {n : ℕ} (hn : 0 < n) (h : finrank ℝ E = n)
+protected def fin_orthonormal_basis (hn : 0 < n) (h : finrank ℝ E = n)
   (x : orientation ℝ E (fin n)) : orthonormal_basis (fin n) ℝ E :=
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
@@ -74,11 +139,134 @@ begin
 end
 
 /-- `orientation.fin_orthonormal_basis` gives a basis with the required orientation. -/
-@[simp] lemma orientation.fin_orthonormal_basis_orientation {n : ℕ} (hn : 0 < n)
+@[simp] lemma fin_orthonormal_basis_orientation (hn : 0 < n)
   (h : finrank ℝ E = n) (x : orientation ℝ E (fin n)) :
   (x.fin_orthonormal_basis hn h).to_basis.orientation = x :=
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
   haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
   exact ((std_orthonormal_basis _ _).reindex $ fin_congr h).orientation_adjust_to_orientation x
 end
+
+section volume_form
+variables [_i : fact (finrank ℝ E = n)] (o : orientation ℝ E (fin n))
+
+include _i o
+
+/-- The volume form on an oriented real inner product space, a nonvanishing top-dimensional
+alternating form uniquely defined by compatibility with the orientation and inner product structure.
+-/
+@[irreducible] def volume_form : alternating_map ℝ E ℝ (fin n) :=
+begin
+  classical,
+  unfreezingI { cases n },
+  { let opos : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (1:ℝ),
+    let oneg : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (-1:ℝ),
+    exact o.eq_or_eq_neg_of_is_empty.by_cases (λ _, opos) (λ _, oneg) },
+  { exact (o.fin_orthonormal_basis n.succ_pos _i.out).to_basis.det }
+end
+
+omit _i o
+
+@[simp] lemma volume_form_zero_pos [_i : fact (finrank ℝ E = 0)] :
+  orientation.volume_form (positive_orientation : orientation ℝ E (fin 0))
+  = alternating_map.const_linear_equiv_of_is_empty 1 :=
+by simp [volume_form, or.by_cases, dif_pos]
+
+@[simp] lemma volume_form_zero_neg [_i : fact (finrank ℝ E = 0)] :
+  orientation.volume_form (-positive_orientation : orientation ℝ E (fin 0))
+  = alternating_map.const_linear_equiv_of_is_empty (-1) :=
+begin
+  dsimp [volume_form, or.by_cases, positive_orientation],
+  apply if_neg,
+  rw [ray_eq_iff, same_ray_comm],
+  intros h,
+  simpa using
+    congr_arg alternating_map.const_linear_equiv_of_is_empty.symm (eq_zero_of_same_ray_self_neg h),
+end
+
+include _i o
+
+/-- 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. -/
+lemma volume_form_robust (b : orthonormal_basis (fin n) ℝ E) (hb : b.to_basis.orientation = o) :
+  o.volume_form = b.to_basis.det :=
+begin
+  unfreezingI { cases n },
+  { have : o = positive_orientation := hb.symm.trans b.to_basis.orientation_is_empty,
+    simp [volume_form, or.by_cases, dif_pos this] },
+  { dsimp [volume_form],
+    rw [same_orientation_iff_det_eq_det, hb],
+    exact o.fin_orthonormal_basis_orientation _ _ },
+end
+
+lemma volume_form_robust' (b : orthonormal_basis (fin n) ℝ E) (v : fin n → E) :
+  |o.volume_form v| = |b.to_basis.det v| :=
+begin
+  unfreezingI { cases n },
+  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  { rw [o.volume_form_robust (b.adjust_to_orientation o) (b.orientation_adjust_to_orientation o),
+      b.abs_det_adjust_to_orientation] },
+end
+
+/-- Let `v` be an indexed family of `n` vectors in an oriented `n`-dimensional real inner
+product space `E`. The output of the volume form of `E` when evaluated on `v` is bounded in absolute
+value by the product of the norms of the vectors `v i`. -/
+lemma abs_volume_form_apply_le (v : fin n → E) : |o.volume_form v| ≤ ∏ i : fin n, ∥v i∥ :=
+begin
+  unfreezingI { cases n },
+  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  haveI : finite_dimensional ℝ E := fact_finite_dimensional_of_finrank_eq_succ n,
+  have : finrank ℝ E = fintype.card (fin n.succ) := by simpa using _i.out,
+  let b : orthonormal_basis (fin n.succ) ℝ E := gram_schmidt_orthonormal_basis this v,
+  have hb : b.to_basis.det v = ∏ i, ⟪b i, v i⟫ := gram_schmidt_orthonormal_basis_det this v,
+  rw [o.volume_form_robust' b, hb, finset.abs_prod],
+  apply finset.prod_le_prod,
+  { intros i hi,
+    positivity },
+  intros i hi,
+  convert abs_real_inner_le_norm (b i) (v i),
+  simp [b.orthonormal.1 i],
+end
+
+lemma volume_form_apply_le (v : fin n → E) : o.volume_form v ≤ ∏ i : fin n, ∥v i∥ :=
+(le_abs_self _).trans (o.abs_volume_form_apply_le v)
+
+/-- Let `v` be an indexed family of `n` orthogonal vectors in an oriented `n`-dimensional
+real inner product space `E`. The output of the volume form of `E` when evaluated on `v` is, up to
+sign, the product of the norms of the vectors `v i`. -/
+lemma abs_volume_form_apply_of_pairwise_orthogonal
+  {v : fin n → E} (hv : pairwise (λ i j, ⟪v i, v j⟫ = 0)) :
+  |o.volume_form v| = ∏ i : fin n, ∥v i∥ :=
+begin
+  unfreezingI { cases n },
+  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp },
+  haveI : finite_dimensional ℝ E := fact_finite_dimensional_of_finrank_eq_succ n,
+  have hdim : finrank ℝ E = fintype.card (fin n.succ) := by simpa using _i.out,
+  let b : orthonormal_basis (fin n.succ) ℝ E := gram_schmidt_orthonormal_basis hdim v,
+  have hb : b.to_basis.det v = ∏ i, ⟪b i, v i⟫ := gram_schmidt_orthonormal_basis_det hdim v,
+  rw [o.volume_form_robust' b, hb, finset.abs_prod],
+  by_cases h : ∃ i, v i = 0,
+  obtain ⟨i, hi⟩ := h,
+  { rw [finset.prod_eq_zero (finset.mem_univ i), finset.prod_eq_zero (finset.mem_univ i)];
+    simp [hi] },
+  push_neg at h,
+  congr,
+  ext i,
+  have hb : b i = ∥v i∥⁻¹ • v i := gram_schmidt_orthonormal_basis_apply_of_orthogonal hdim hv (h i),
+  simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, is_R_or_C.conj_to_real],
+  rw abs_of_nonneg,
+  { have : ∥v i∥ ≠ 0 := by simpa using h i,
+    field_simp },
+  { positivity },
+end
+
+/-- The output of the volume form of an oriented real inner product space `E` when evaluated on an
+orthonormal basis is ±1. -/
+lemma abs_volume_form_apply_of_orthonormal (v : orthonormal_basis (fin n) ℝ E) :
+  |o.volume_form v| = 1 :=
+by simpa [o.volume_form_robust' v v] using congr_arg abs v.to_basis.det_self
+
+end volume_form
+
+end orientation

src/linear_algebra/determinant.lean

@@ -454,6 +454,12 @@ lemma basis.det_apply (v : ι → M) : e.det v = det (e.to_matrix v) := rfl
 lemma basis.det_self : e.det e = 1 :=
 by simp [e.det_apply]
 
+@[simp] lemma basis.det_is_empty [is_empty ι] : e.det = alternating_map.const_of_is_empty R M 1 :=
+begin
+  ext v,
+  exact matrix.det_is_empty,
+end
+
 /-- `basis.det` is not the zero map. -/
 lemma basis.det_ne_zero [nontrivial R] : e.det ≠ 0 :=
 λ h, by simpa [h] using e.det_self

src/linear_algebra/orientation.lean

@@ -50,6 +50,8 @@ abbreviation orientation := module.ray R (alternating_map R M R ι)
 class module.oriented :=
 (positive_orientation : orientation R M ι)
 
+export module.oriented (positive_orientation)
+
 variables {R M}
 
 /-- An equivalence between modules implies an equivalence between orientations. -/
@@ -68,6 +70,12 @@ by rw [orientation.map, alternating_map.dom_lcongr_refl, module.ray.map_refl]
 @[simp] lemma orientation.map_symm (e : M ≃ₗ[R] N) :
   (orientation.map ι e).symm = orientation.map ι e.symm := rfl
 
+/-- A module is canonically oriented with respect to an empty index type. -/
+@[priority 100] instance is_empty.oriented [nontrivial R] [is_empty ι] :
+  module.oriented R M ι :=
+{ positive_orientation := ray_of_ne_zero R (alternating_map.const_linear_equiv_of_is_empty 1) $
+    alternating_map.const_linear_equiv_of_is_empty.injective.ne (by simp) }
+
 end ordered_comm_semiring
 
 section ordered_comm_ring
@@ -113,6 +121,13 @@ begin
   simp
 end
 
+@[simp] lemma orientation_is_empty [nontrivial R] [is_empty ι] (b : basis ι R M) :
+  b.orientation = positive_orientation :=
+begin
+  congrm ray_of_ne_zero _ _ _,
+  convert b.det_is_empty,
+end
+
 end basis
 
 end ordered_comm_ring
@@ -123,6 +138,31 @@ variables {R : Type*} [linear_ordered_comm_ring R]
 variables {M : Type*} [add_comm_group M] [module R M]
 variables {ι : Type*} [decidable_eq ι]
 
+namespace orientation
+
+/-- A module `M` over a linearly ordered commutative ring has precisely two "orientations" with
+respect to an empty index type. (Note that these are only orientations of `M` of in the conventional
+mathematical sense if `M` is zero-dimensional.) -/
+lemma eq_or_eq_neg_of_is_empty [nontrivial R] [is_empty ι] (o : orientation R M ι) :
+  o = positive_orientation ∨ o = - positive_orientation :=
+begin
+  induction o using module.ray.ind with x hx,
+  dsimp [positive_orientation],
+  simp only [ray_eq_iff, same_ray_neg_swap],
+  rw same_ray_or_same_ray_neg_iff_not_linear_independent,
+  intros h,
+  let a : R := alternating_map.const_linear_equiv_of_is_empty.symm x,
+  have H : linear_independent R ![a, 1],
+  { convert h.map' ↑alternating_map.const_linear_equiv_of_is_empty.symm (linear_equiv.ker _),
+    ext i,
+    fin_cases i;
+    simp [a] },
+  rw linear_independent_iff' at H,
+  simpa using H finset.univ ![1, -a] (by simp [fin.sum_univ_succ]) 0 (by simp),
+end
+
+end orientation
+
 namespace basis
 
 variables [fintype ι]