OAI/Geometry/EinsteinFour/GradientPairing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Bilinear compression on the actual Bianchi gradient space.

  1. abbrev OAI.PositiveEinsteinFour.Bianchi.GradientIndex line 16
  2. def OAI.PositiveEinsteinFour.Bianchi.rawCoordinates line 18
  3. def OAI.PositiveEinsteinFour.Bianchi.rawPairing line 20
  4. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_comm line 23
  5. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_vectors line 26
  6. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_add_left line 39
  7. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_add_right line 45
  8. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_sum_left line 49
  9. def OAI.PositiveEinsteinFour.Bianchi.rawCoupling line 60
  10. def OAI.PositiveEinsteinFour.Bianchi.gradientCouplingKernel line 63
  11. theorem OAI.PositiveEinsteinFour.Bianchi.gradientCouplingKernel_symmetric line 68
  12. theorem OAI.PositiveEinsteinFour.Bianchi.rawCoupling_coordinates line 79
  13. theorem OAI.PositiveEinsteinFour.Bianchi.rawCoupling_selfadjoint line 114
  14. theorem OAI.PositiveEinsteinFour.Bianchi.rawCoupling_matrix line 125
  15. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_smul_left line 127
  16. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_smul_right line 132
  17. theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_sub_left line 137
  18. theorem OAI.PositiveEinsteinFour.Bianchi.gradientProjection_pairing line 145

    Source documentation

    Pairing with a genuine Bianchi tensor removes the displayed polynomial projection, by self-adjointness of the actual finite-dimensional coupling.

    theorem gradientProjection_pairing (Z W : Tensor) (hw : W.bianchi) :
    rawPairing (gradientProjection Z) W.matrix = rawPairing Z.matrix W.matrix := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.gradientProjection

  19. theorem OAI.PositiveEinsteinFour.Bianchi.derivativeQuaternion_pairing line 159

    Source documentation

    The derivative-slot quaternion has the actual one-fifth compression against any other Bianchi gradient, retaining both bilinear arguments.

    theorem derivativeQuaternion_pairing (r : Fin 3) (Z W : Tensor)
    (hz : Z.bianchi) (hw : W.bianchi) :
    rawPairing (derivativeQuaternion r Z).matrix W.matrix =
      (1 / 5 : ℝ) * rawPairing (rawGradientGenerator r Z.matrix) W.matrix := by
…

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