OrthogonalCompression.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Determinant compression after an orthogonal change of basis.

theorem OAI.PositiveEinsteinFour.Jacobi.orthogonal_extension line 16

Source documentation

Complete orthonormal columns to an orthogonal matrix while keeping each prescribed column in its original position.

theorem orthogonal_extension {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (W : Matrix (m ⊕ n) m ℝ) (hW : Wᴴ * W = 1) :
    ∃ U : Matrix (m ⊕ n) (m ⊕ n) ℝ,
      U * Uᴴ = 1 ∧ ∀ i j, U i (Sum.inl j) = W i j := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.trace_sum_blocks line 44

theorem OAI.PositiveEinsteinFour.Jacobi.det_le_orthogonal_compression line 52

Source documentation

The determinant loss depends on the first compression and total trace, not on the choice of an orthonormal basis of its complement.

theorem det_le_orthogonal_compression {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    {A U : Matrix (m ⊕ n) (m ⊕ n) ℝ}
    (hA : A.PosDef) (hU : U * Uᴴ = 1)
    (htrace : A.trace ≤ Fintype.card m + Fintype.card n)
    (hfirst : (Uᴴ * A * U).toBlocks₁₁.trace = Fintype.card m) :
    A.det ≤ (Uᴴ * A * U).toBlocks₁₁.det := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.det_le_isometric_compression line 94

Source documentation

An orthonormal family of columns is enough to apply the determinant comparison; the complementary basis is constructed, not assumed.

theorem det_le_isometric_compression {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    {A : Matrix (m ⊕ n) (m ⊕ n) ℝ} (W : Matrix (m ⊕ n) m ℝ)
    (hA : A.PosDef) (hW : Wᴴ * W = 1)
    (htrace : A.trace ≤ Fintype.card m + Fintype.card n)
    (hfirst : (Wᴴ * A * W).trace = Fintype.card m) :
    A.det ≤ (Wᴴ * A * W).det := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.det_le_isometric_compression_of_card line 110

Source documentation

Reindexing version for a matrix whose ambient coordinates need not already separate the distinguished columns from their complement.

theorem det_le_isometric_compression_of_card {I m n : Type*}
    [Fintype I] [Fintype m] [Fintype n]
    [DecidableEq I] [DecidableEq m] [DecidableEq n]
    (hcard : Fintype.card I = Fintype.card m + Fintype.card n)
    {A : Matrix I I ℝ} (W : Matrix I m ℝ)
    (hA : A.PosDef) (hW : Wᴴ * W = 1)
    (htrace : A.trace ≤ Fintype.card I)
    (hfirst : (Wᴴ * A * W).trace = Fintype.card m) :
    A.det ≤ (Wᴴ * A * W).det := by
…