JacobiCompression.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Trace calculations for normalizing the finite Jacobi matrix.

def OAI.PositiveEinsteinFour.Jacobi.scalarLift line 15
theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_mul line 19
theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_one line 24
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_scalarLift line 27
theorem OAI.PositiveEinsteinFour.Jacobi.trace_eq_sum_block_traces line 33
theorem OAI.PositiveEinsteinFour.Jacobi.trace_scalarLift_mul_diagonal line 41
Source documentation
A scalar operation on the time nodes pairs only with the trace of each normal curvature block. Cross-time commutation is not used.
```
theorem trace_scalarLift_mul_diagonal {N : ℕ} (G : Matrix (Fin N) (Fin N) ℝ)
    (A : Fin N → NormalMatrix) :
    (scalarLift G * Matrix.blockDiagonal A).trace = ∑ i, G i i * (A i).trace := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.scalarLift
theorem OAI.PositiveEinsteinFour.Jacobi.trace_normalized_defect_zero line 50
Source documentation
The normalized perturbation has trace zero whenever every Weyl block has trace zero, for any scalar time-node normalizer.
```
theorem trace_normalized_defect_zero {N : ℕ} (G : Matrix (Fin N) (Fin N) ℝ)
    (A : Fin N → NormalMatrix) (hA : ∀ i, (A i).trace = 0) :
    (scalarLift G * Matrix.blockDiagonal A * scalarLift G).trace = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.scalarLift
theorem OAI.PositiveEinsteinFour.Jacobi.normalized_jacobi_trace line 58
Source documentation
The trace of the normalized Jacobi matrix is precisely its dimension. This is the trace bound used on the complementary block in compression.
```
theorem normalized_jacobi_trace {N : ℕ} (G L : Matrix (Fin N) (Fin N) ℝ)
    (A : Fin N → NormalMatrix) (a : ℝ)
    (hG : G * L * G = 1) (hA : ∀ i, (A i).trace = 0) :
    (scalarLift G * (scalarLift L - a ^ 2 • Matrix.blockDiagonal A) * scalarLift G).trace =
      3 * N := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.scalarLift