ModeCompression.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Compression onto a common scalar time mode in the three normal directions.

def OAI.PositiveEinsteinFour.Jacobi.modeEmbedding line 13
theorem OAI.PositiveEinsteinFour.Jacobi.mul_modeEmbedding line 16
theorem OAI.PositiveEinsteinFour.Jacobi.mode_compression_apply line 22
theorem OAI.PositiveEinsteinFour.Jacobi.mode_compression_diagonal line 41
theorem OAI.PositiveEinsteinFour.Jacobi.mode_compression_scalar line 54
theorem OAI.PositiveEinsteinFour.Jacobi.modeEmbedding_orthonormal line 69
Source documentation
Every unit time mode yields three orthonormal columns.
```
theorem modeEmbedding_orthonormal {N : ℕ} (w : Fin N → ℝ)
    (hw : ∑ i, w i ^ 2 = 1) :
    (modeEmbedding w)ᵀ * modeEmbedding w = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.modeEmbedding
theorem OAI.PositiveEinsteinFour.Jacobi.trace_mode_compression_defect line 77
Source documentation
Trace-free Weyl blocks give a trace-free compressed perturbation.
```
theorem trace_mode_compression_defect {N : ℕ} (A : Fin N → NormalMatrix)
    (w : Fin N → ℝ) (hA : ∀ i, (A i).trace = 0) :
    ((modeEmbedding w)ᵀ * Matrix.blockDiagonal A * modeEmbedding w).trace = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.modeEmbedding
theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_mode_eigenvector line 83

theorem OAI.PositiveEinsteinFour.Jacobi.normalized_mode_compression line 97

Source documentation

The first-mode block of the normalized Jacobi matrix is exactly the weighted curvature average.

theorem normalized_mode_compression {N : ℕ}
    (G L : Matrix (Fin N) (Fin N) ℝ) (A : Fin N → NormalMatrix)
    (w : Fin N → ℝ) (a g : ℝ)
    (hw : ∑ i, w i ^ 2 = 1) (hGsymm : Gᵀ = G) (hG : G * L * G = 1)
    (heigen : G *ᵥ w = g • w) :
    (modeEmbedding w)ᵀ *
        (scalarLift G * (scalarLift L - a ^ 2 • Matrix.blockDiagonal A) * scalarLift G) *
        modeEmbedding w =
      (1 : NormalMatrix) - (a * g) ^ 2 • (∑ i, w i ^ 2 • A i) := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.modeEmbedding, OAI.PositiveEinsteinFour.Jacobi.scalarLift