Documentation

Mathlib.Analysis.InnerProductSpace.Orientation

Orientations of real inner product spaces. #

This file provides definitions and proves lemmas about orientations of real inner product spaces.

Main definitions #

Main theorems #

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (f : OrthonormalBasis ι E) (h : e.toBasis.orientation = f.toBasis.orientation) :
e.toBasis.det f = 1

The change-of-basis matrix between two orthonormal bases with the same orientation has determinant 1.

theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (f : OrthonormalBasis ι E) (h : e.toBasis.orientation f.toBasis.orientation) :
e.toBasis.det f = -1

The change-of-basis matrix between two orthonormal bases with the opposite orientations has determinant -1.

theorem OrthonormalBasis.same_orientation_iff_det_eq_det {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : OrthonormalBasis ι E} {f : OrthonormalBasis ι E} :
e.toBasis.det = f.toBasis.det e.toBasis.orientation = f.toBasis.orientation

Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional form on E, and conversely.

theorem OrthonormalBasis.det_eq_neg_det_of_opposite_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (f : OrthonormalBasis ι E) (h : e.toBasis.orientation f.toBasis.orientation) :
e.toBasis.det = -f.toBasis.det

Two orthonormal bases with opposite orientations determine opposite "determinant" top-dimensional forms on E.

theorem OrthonormalBasis.orthonormal_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] :
Orthonormal (e.toBasis.adjustToOrientation x)

OrthonormalBasis.adjustToOrientation, applied to an orthonormal basis, preserves the property of orthonormality.

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.

Equations
  • e.adjustToOrientation x = (e.toBasis.adjustToOrientation x).toOrthonormalBasis
Instances For
    theorem OrthonormalBasis.toBasis_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] :
    (e.adjustToOrientation x).toBasis = e.toBasis.adjustToOrientation x
    @[simp]
    theorem OrthonormalBasis.orientation_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] :
    (e.adjustToOrientation x).toBasis.orientation = x

    adjustToOrientation gives an orthonormal basis with the required orientation.

    theorem OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] (i : ι) :
    (e.adjustToOrientation x) i = e i (e.adjustToOrientation x) i = -e i

    Every basis vector from adjustToOrientation is either that from the original basis or its negation.

    theorem OrthonormalBasis.det_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] :
    (e.adjustToOrientation x).toBasis.det = e.toBasis.det (e.adjustToOrientation x).toBasis.det = -e.toBasis.det
    theorem OrthonormalBasis.abs_det_adjustToOrientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι E) (x : Orientation E ι) [Nonempty ι] (v : ιE) :
    |(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|

    An orthonormal basis, indexed by Fin n, with the given orientation.

    Equations
    Instances For
      @[simp]
      theorem Orientation.finOrthonormalBasis_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } (hn : 0 < n) (h : Module.finrank E = n) (x : Orientation E (Fin n)) :
      (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

      Orientation.finOrthonormalBasis gives a basis with the required orientation.

      @[irreducible]

      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.

      Equations
      Instances For
        theorem Orientation.volumeForm_def {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) :
        o.volumeForm = Nat.casesAuxOn (motive := fun (a : ) => n = aE [⋀^Fin n]→ₗ[] ) n (fun (h : n = 0) => Eq.ndrec (motive := fun {n : } => [_i : Fact (Module.finrank E = n)] → Orientation E (Fin n)E [⋀^Fin n]→ₗ[] ) (fun [Fact (Module.finrank E = 0)] (o : Orientation E (Fin 0)) => let opos := AlternatingMap.constOfIsEmpty E (Fin 0) 1; .by_cases (fun (x : o = positiveOrientation) => opos) fun (x : o = -positiveOrientation) => -opos) o) (fun (n_1 : ) (h : n = n_1 + 1) => Eq.ndrec (motive := fun {n : } => [_i : Fact (Module.finrank E = n)] → Orientation E (Fin n)E [⋀^Fin n]→ₗ[] ) (fun [Fact (Module.finrank E = n_1 + 1)] (o : Orientation E (Fin (n_1 + 1))) => (Orientation.finOrthonormalBasis o).toBasis.det) o)
        @[simp]
        theorem Orientation.volumeForm_zero_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [_i : Fact (Module.finrank E = 0)] :
        positiveOrientation.volumeForm = AlternatingMap.constLinearEquivOfIsEmpty 1
        theorem Orientation.volumeForm_zero_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [_i : Fact (Module.finrank E = 0)] :
        (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1
        theorem Orientation.volumeForm_robust {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (b : OrthonormalBasis (Fin n) E) (hb : b.toBasis.orientation = o) :
        o.volumeForm = b.toBasis.det

        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 Orientation.volumeForm_robust_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (b : OrthonormalBasis (Fin n) E) (hb : b.toBasis.orientation o) :
        o.volumeForm = -b.toBasis.det

        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.

        @[simp]
        theorem Orientation.volumeForm_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) :
        (-o).volumeForm = -o.volumeForm
        theorem Orientation.volumeForm_robust' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (b : OrthonormalBasis (Fin n) E) (v : Fin nE) :
        |o.volumeForm v| = |b.toBasis.det v|
        theorem Orientation.abs_volumeForm_apply_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (v : Fin nE) :
        |o.volumeForm v| i : Fin n, v i

        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.

        theorem Orientation.volumeForm_apply_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (v : Fin nE) :
        o.volumeForm v i : Fin n, v i
        theorem Orientation.abs_volumeForm_apply_of_pairwise_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) {v : Fin nE} (hv : Pairwise fun (i j : Fin n) => inner (v i) (v j) = 0) :
        |o.volumeForm v| = i : Fin n, v i

        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.

        theorem Orientation.abs_volumeForm_apply_of_orthonormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (v : OrthonormalBasis (Fin n) E) :
        |o.volumeForm v| = 1

        The output of the volume form of an oriented real inner product space E when evaluated on an orthonormal basis is ±1.

        theorem Orientation.volumeForm_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace F] [Fact (Module.finrank F = n)] (φ : E ≃ₗᵢ[] F) (x : Fin nF) :
        ((Orientation.map (Fin n) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (φ.symm x)
        theorem Orientation.volumeForm_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {n : } [_i : Fact (Module.finrank E = n)] (o : Orientation E (Fin n)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (x : Fin nE) :
        o.volumeForm (φ x) = o.volumeForm x

        The volume form is invariant under pullback by a positively-oriented isometric automorphism.