OAI/Geometry/EinsteinFour/AngularRotation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual change of normal bases I_s q and J_t q. Its spherical orthogonality is a consequence of the fourth monomial moment.

  1. def OAI.PositiveEinsteinFour.Angular.oppositeMatrix line 14
  2. def OAI.PositiveEinsteinFour.Angular.mixingCoefficient line 16
  3. def OAI.PositiveEinsteinFour.Angular.coefficientTable line 19
  4. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_eq_table line 22
  5. def OAI.PositiveEinsteinFour.Angular.mixing line 30
  6. def OAI.PositiveEinsteinFour.Angular.mixingMatrix line 33
  7. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_symmetric line 35
  8. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_trace line 43
  9. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_pairing line 49
  10. theorem OAI.PositiveEinsteinFour.Angular.integral_mixing_mul line 56
  11. theorem OAI.PositiveEinsteinFour.Angular.direction_sum_sq line 65
  12. theorem OAI.PositiveEinsteinFour.Angular.mixing_orthogonal line 70

    Source documentation

    The two triples give orthonormal normal bases for every unit direction.

    theorem mixing_orthogonal (q : Directions) :
    mixingMatrix q * (mixingMatrix q)ᵀ = 1 := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.Directions, OAI.PositiveEinsteinFour.Angular.mixingMatrix