QuaternionGenerators.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The rotation of the matrix indices is recovered from the actual quaternion commutator. Thus a four-dimensional quaternion lift also intertwines the three-dimensional infinitesimal rotation generators.

theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_apply line 16
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_entry line 21
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_injective line 26
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_commutator_0 line 33
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_commutator_1 line 44
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_commutator_2 line 55
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_commutator line 68
Source documentation
The speed-two generator in the matrix indices is the commutator of the corresponding unit imaginary quaternion.
```
theorem imaginaryLeft_commutator (s : Fin 3) (v : Fin 3 → ℝ) :
    quaternionMatrix s * imaginaryCombination quaternionMatrix v -
      imaginaryCombination quaternionMatrix v * quaternionMatrix s =
        imaginaryCombination quaternionMatrix (TraceHessian.rotation s *ᵥ v) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination, OAI.PositiveEinsteinFour.TraceHessian.rotation
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_general_commutator line 77
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.mul_transpose line 100
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rotation_intertwines line 107
Source documentation
The matrix rotation generators transform under exactly the same three-dimensional frame change as the imaginary quaternion basis.
```
theorem QuaternionLift.rotation_intertwines {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R) (s : Fin 3) :
    R * TraceHessian.rotation s =
      (∑ r, R r s • TraceHessian.rotation r) * R := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.TraceHessian.rotation