GradientCoordinates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quadratic compression in the fixed Bianchi coordinate model.

theorem OAI.PositiveEinsteinFour.Bianchi.generator_row_energy line 15
Source documentation
Direct quadratic compression on actual Bianchi tensors.
```
theorem generator_row_energy (s : Fin 3) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ a, ∑ b, ‖rawGradientGenerator s Z.matrix a b‖ ^ 2) +
      40 * (∑ b, ‖Z.matrix s b‖ ^ 2) = 25 * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator

theorem OAI.PositiveEinsteinFour.Bianchi.weighted_generator_matrixForm line 42

Source documentation

Contracting the actual generators gives the diagonal matrix-slot form.

theorem weighted_generator_matrixForm (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    -(∑ s, t s * (∑ a, ∑ b, ‖rawGradientGenerator s Z.matrix a b‖ ^ 2)) / 40 =
      ∑ s, t s * (∑ b, ‖Z.matrix s b‖ ^ 2) := by
…

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