OAI/Geometry/EinsteinFour/GradientOperator.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Actual generator commutators on the Bianchi gradient coordinates.

  1. abbrev OAI.PositiveEinsteinFour.Bianchi.RawGradient line 14
  2. def OAI.PositiveEinsteinFour.Bianchi.rawMatrixRotation line 16
  3. def OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator line 19
  4. theorem OAI.PositiveEinsteinFour.Bianchi.rawMatrixRotation_matrix line 22
  5. theorem OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator_matrix line 25
  6. theorem OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator_add line 28
  7. theorem OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator_smul line 35
  8. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_0_0 line 41
  9. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_0_1 line 50
  10. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_0_2 line 59
  11. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_1_0 line 68
  12. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_1_1 line 77
  13. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_1_2 line 86
  14. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_2_0 line 95
  15. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_2_1 line 104
  16. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_commutator_2_2 line 113
  17. theorem OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator_commutator line 123

    Source documentation

    The three actual total generators obey the quaternion rotation bracket.

    theorem rawGradientGenerator_commutator (s : Fin 3) (Z : RawGradient) :
    rawGradientGenerator s (rawGradientGenerator (next s) Z) -
      rawGradientGenerator (next s) (rawGradientGenerator s Z) =
        (2 : ℝ) • rawGradientGenerator (previous s) Z := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator, OAI.PositiveEinsteinFour.Bianchi.next, OAI.PositiveEinsteinFour.Bianchi.previous

  18. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_0_0 line 139
  19. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_0_1 line 152
  20. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_0_2 line 164
  21. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_1_0 line 176
  22. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_1_1 line 188
  23. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_1_2 line 201
  24. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_2_0 line 213
  25. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_2_1 line 225
  26. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_2_2 line 237
  27. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_0 line 250
  28. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_1 line 259
  29. theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_casimir_2 line 268
  30. theorem OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator_casimir line 278

    Source documentation

    The pointwise Casimir identity follows from the actual trace and Bianchi equations.

    theorem rawGradientGenerator_casimir (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi)
    (a b : Fin 3) :
    (∑ s : Fin 3, rawGradientGenerator s (rawGradientGenerator s Z.matrix) a b) =
      (-35 : ℝ) • Z.matrix a b := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator