OAI/Geometry/EinsteinFour/SphericalPairMix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A forty-five degree orthogonal change in a coordinate plane. This fixed finite-dimensional change gives the fourth and sixth sphere moments.

  1. def OAI.PositiveEinsteinFour.Angular.pairMixLinear line 14
  2. theorem OAI.PositiveEinsteinFour.Angular.pairMix_apply line 40
  3. theorem OAI.PositiveEinsteinFour.Angular.pairMix_norm line 44
  4. theorem OAI.PositiveEinsteinFour.Angular.pairMix_involutive line 67
  5. def OAI.PositiveEinsteinFour.Angular.pairMix line 86
  6. theorem OAI.PositiveEinsteinFour.Angular.pairMix_coordinate line 94