RicciMatrixChange.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Tracing curvature after an arbitrary invertible change of coordinates.

def OAI.PositiveEinsteinFour.Geometry.ricciMatrix line 15
Source documentation
Contract the output and first curvature-input indices.
```
def ricciMatrix (R : Fin 4 → Fin 4 → Mat4) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.conjugate_row_contraction line 18
theorem OAI.PositiveEinsteinFour.Geometry.ricciMatrix_pullback line 29
Source documentation
Curvature conjugation in the vector slot and the two covector slots induces precisely the ordinary covariant matrix law for Ricci.
```
theorem ricciMatrix_pullback (J : Mat4) (R S : Fin 4 → Fin 4 → Mat4)
    (hJ : IsUnit J.det)
    (hS : ∀ i j, S i j = J⁻¹ *
      (∑ a, ∑ b, (J a i * J b j) • R a b) * J) :
    ricciMatrix S = Jᵀ * (ricciMatrix R * J) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.ricciMatrix