OAI/Geometry/EinsteinFour/GeneralMatrixCompression.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Bianchi compression for an arbitrary symmetric trace-free Weyl matrix, with no choice of a moving diagonal frame.

  1. def OAI.PositiveEinsteinFour.Bianchi.generalMatrixAction line 18

    Source documentation

    The actual trace-free anticommutator, acting on the two matrix indices.

    def generalMatrixAction (A : Mat) (Z : RawGradient) : RawGradient :=
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient

  2. def OAI.PositiveEinsteinFour.Bianchi.generalMixedAction line 22

    Source documentation

    Mixed derivative/matrix action, retaining the full matrix of coefficients.

    def generalMixedAction (A : Mat) (Z : RawGradient) : RawGradient :=
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient

  3. def OAI.PositiveEinsteinFour.Bianchi.costMatrix line 26
  4. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_0_0 line 36
  5. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_0_1 line 44
  6. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_0_2 line 51
  7. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_1_0 line 59
  8. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_1_1 line 66
  9. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_1_2 line 74
  10. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_2_0 line 82
  11. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_2_1 line 90
  12. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq_2_2 line 98
  13. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_eq line 105
  14. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_0_0 line 120
  15. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_0_1 line 130
  16. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_0_2 line 140
  17. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_0_3 line 150
  18. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_0 line 160
  19. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_1_0 line 171
  20. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_1_1 line 181
  21. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_1_2 line 191
  22. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_1_3 line 201
  23. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_1 line 211
  24. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_2_0 line 222
  25. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_2_1 line 232
  26. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_2_2 line 242
  27. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_2_3 line 252
  28. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_0_2 line 262
  29. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_0_0 line 273
  30. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_0_1 line 283
  31. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_0_2 line 293
  32. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_0_3 line 303
  33. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_0 line 313
  34. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_1_0 line 324
  35. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_1_1 line 334
  36. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_1_2 line 344
  37. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_1_3 line 354
  38. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_1 line 364
  39. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_2_0 line 375
  40. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_2_1 line 385
  41. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_2_2 line 395
  42. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_2_3 line 405
  43. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_1_2 line 415
  44. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_0_0 line 426
  45. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_0_1 line 436
  46. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_0_2 line 446
  47. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_0_3 line 456
  48. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_0 line 466
  49. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_1_0 line 477
  50. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_1_1 line 487
  51. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_1_2 line 497
  52. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_1_3 line 507
  53. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_1 line 517
  54. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_2_0 line 528
  55. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_2_1 line 538
  56. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_2_2 line 548
  57. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_2_3 line 558
  58. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates_2_2 line 568
  59. theorem OAI.PositiveEinsteinFour.Bianchi.coupling_matrix_coordinates line 580
  60. theorem OAI.PositiveEinsteinFour.Bianchi.rawCoupling_generalMatrixAction line 599

    Source documentation

    The full coefficient matrix satisfies the same coupling identity as the diagonal specialization. The proof uses the actual twelve-dimensional Bianchi coordinates and the five free entries of the symmetric matrix.

    theorem rawCoupling_generalMatrixAction (A : Mat)
    (hA : symmetric A) (hAt : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    rawCoupling (generalMatrixAction A Z.matrix) =
      (-(1 / 2 : ℝ)) • generalMixedAction A Z.matrix := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawCoupling, OAI.PositiveEinsteinFour.Bianchi.generalMatrixAction, OAI.PositiveEinsteinFour.Bianchi.generalMixedAction

  61. theorem OAI.PositiveEinsteinFour.Bianchi.generalMixedAction_pairing line 610

    Source documentation

    Bilinear compression against any Bianchi test tensor. No pointwise diagonal frame is assumed for either the Weyl coefficient or the test.

    theorem generalMixedAction_pairing (A : Mat)
    (hA : symmetric A) (hAt : traceFree A)
    (Z W : Tensor) (hz : Z.traceFree) (hbz : Z.bianchi) (hbw : W.bianchi) :
    rawPairing (generalMixedAction A Z.matrix) W.matrix =
      8 * rawPairing (generalMatrixAction A Z.matrix) W.matrix := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.generalMixedAction, OAI.PositiveEinsteinFour.Bianchi.generalMatrixAction

  62. def OAI.PositiveEinsteinFour.Bianchi.rawBianchiProjection line 624

    Source documentation

    The polynomial formula for the actual orthogonal Bianchi compression.

    def rawBianchiProjection (Z : RawGradient) : RawGradient :=
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient

  63. theorem OAI.PositiveEinsteinFour.Bianchi.rawBianchiProjection_pairing line 627
  64. theorem OAI.PositiveEinsteinFour.Bianchi.generalRicci_compression line 639

    Source documentation

    The uncompressed Ricci expression equals 13Z−20P(B_F(A)Z) as an actual four-vector-valued array, for arbitrary Weyl coefficients.

    theorem generalRicci_compression (A : Mat)
    (hA : symmetric A) (hAt : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (13 : ℝ) • Z.matrix - (12 : ℝ) • generalMatrixAction A Z.matrix -
        generalMixedAction A Z.matrix =
      (13 : ℝ) • Z.matrix -
        (20 : ℝ) • rawBianchiProjection (generalMatrixAction A Z.matrix) := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.generalMatrixAction, OAI.PositiveEinsteinFour.Bianchi.generalMixedAction, OAI.PositiveEinsteinFour.Bianchi.rawBianchiProjection