OAI/Geometry/EinsteinFour/GradientCoordinateModel.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Fixed twelve real coordinates for the inner generators in the cost calculation.

  1. def OAI.PositiveEinsteinFour.Bianchi.costShape line 14
  2. def OAI.PositiveEinsteinFour.Bianchi.costParameters line 20

    Source documentation

    Only this fixed frame is needed for the invariant real-vector cost.

    def costParameters (v : Fin 3 → Vec) : Tensor := parameters costShape (v 0) (v 1) (v 2)

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.costShape

  3. def OAI.PositiveEinsteinFour.Bianchi.generatorCoefficients line 22
  4. def OAI.PositiveEinsteinFour.Bianchi.generatorCoordinates line 27
  5. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_0_0 line 30
  6. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_0_1 line 40
  7. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_0_2 line 50
  8. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_1_0 line 60
  9. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_1_1 line 70
  10. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_1_2 line 80
  11. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_2_0 line 90
  12. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_2_1 line 100
  13. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates_2_2 line 110
  14. theorem OAI.PositiveEinsteinFour.Bianchi.generator_coordinates line 121

    Source documentation

    Exact generator action in the fixed Bianchi coordinate frame.

    theorem generator_coordinates (s : Fin 3) (v : Fin 3 → Vec) :
    rawGradientGenerator s (costParameters v).matrix =
      (costParameters (generatorCoordinates s v)).matrix := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator, OAI.PositiveEinsteinFour.Bianchi.costParameters, OAI.PositiveEinsteinFour.Bianchi.generatorCoordinates

  15. theorem OAI.PositiveEinsteinFour.Bianchi.exists_costParameters line 137

    Source documentation

    The fixed coordinates cover every trace-free Bianchi tensor.

    theorem exists_costParameters (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    ∃ v : Fin 3 → Vec, costParameters v = Z := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.costParameters

  16. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_add line 143
  17. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_smul line 152
  18. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_neg line 160
  19. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_matrix_sub line 164
  20. def OAI.PositiveEinsteinFour.Bianchi.coordinateNorm line 172

    Source documentation

    The actual Frobenius norm in these twelve real coordinates.

    def coordinateNorm (v : Fin 3 → Vec) : ℝ :=
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec

  21. theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_norm line 175
  22. def OAI.PositiveEinsteinFour.Bianchi.costCoefficientCoordinates line 182

    Source documentation

    The three quaternion coefficients of the total action on (7-K)L.

    def costCoefficientCoordinates (s r : Fin 3) (v : Fin 3 → Vec) : Fin 3 → Vec :=
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec

  23. theorem OAI.PositiveEinsteinFour.Bianchi.generator_norm_0 line 190
  24. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_0_0 line 200
  25. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_0_1 line 211
  26. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_0_2 line 222
  27. theorem OAI.PositiveEinsteinFour.Bianchi.generator_norm_1 line 233
  28. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_1_0 line 243
  29. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_1_1 line 254
  30. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_1_2 line 265
  31. theorem OAI.PositiveEinsteinFour.Bianchi.generator_norm_2 line 276
  32. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_2_0 line 286
  33. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_2_1 line 297
  34. theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_norm_2_2 line 308
  35. theorem OAI.PositiveEinsteinFour.Bianchi.costCoefficient_norm_0 line 319
  36. theorem OAI.PositiveEinsteinFour.Bianchi.costCoefficient_norm_1 line 328
  37. theorem OAI.PositiveEinsteinFour.Bianchi.costCoefficient_norm_2 line 337
  38. theorem OAI.PositiveEinsteinFour.Bianchi.costCoefficient_norm line 347

    Source documentation

    The scalar matrix certificate yielding the real-vector curvature cost.

    theorem costCoefficient_norm (s : Fin 3) (v : Fin 3 → Vec) :
    64 * coordinateNorm (generatorCoordinates s v) +
      (∑ r : Fin 3, coordinateNorm (costCoefficientCoordinates s r v)) =
        84 * coordinateNorm v + 108 * coordinateNorm (generatorCoordinates s v) := by
…

    Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.coordinateNorm, OAI.PositiveEinsteinFour.Bianchi.generatorCoordinates, OAI.PositiveEinsteinFour.Bianchi.costCoefficientCoordinates

  39. theorem OAI.PositiveEinsteinFour.Bianchi.row_norm_0 line 357
  40. theorem OAI.PositiveEinsteinFour.Bianchi.row_norm_1 line 367
  41. theorem OAI.PositiveEinsteinFour.Bianchi.row_norm_2 line 377