Gram.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact rational Gram witnesses

A unit lower triangular matrix and a positive rational diagonal certify a real matrix's positive definiteness. The large numerical checks can therefore be split into separate rational identities for individual matrix entries.

def OAI.MUB6.Certificate.lowerUnit line 21
Source documentation
Complete a table of strict lower triangular entries with unit diagonal.
```
def lowerUnit {n : ℕ} (entries : Matrix (Fin n) (Fin n) ℚ) :
    Matrix (Fin n) (Fin n) ℚ :=
…
```

def OAI.MUB6.Certificate.realMatrix line 26

Source documentation

Interpret a rational matrix as a real matrix.

def realMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) :
    Matrix (Fin n) (Fin n) ℝ := fun i j => A i j

theorem OAI.MUB6.Certificate.lowerUnit_diag line 29
theorem OAI.MUB6.Certificate.lowerUnit_above line 32
theorem OAI.MUB6.Certificate.real_lowerUnit_det line 36

theorem OAI.MUB6.Certificate.real_gram_eq line 47

Source documentation

A collection of scalar rational checks certifies the full real Gram identity.

theorem real_gram_eq {n : ℕ} (Z U : Matrix (Fin n) (Fin n) ℚ) (D : Fin n → ℚ)
    (h : ∀ i j, Z i j = ∑ k, U k i * D k * U k j) :
    realMatrix Z = (realMatrix U)ᴴ * Matrix.diagonal (fun k => (D k : ℝ)) * realMatrix U := by
…

Mentions: OAI.MUB6.Certificate.realMatrix

theorem OAI.MUB6.Certificate.posDef_of_rational_gram line 57

Source documentation

Soundness of a positive diagonal/unit-triangular Gram certificate.

theorem posDef_of_rational_gram {n : ℕ}
    (Z entries : Matrix (Fin n) (Fin n) ℚ) (D : Fin n → ℚ)
    (hD : ∀ i, 0 < D i)
    (hZ : ∀ i j, Z i j = ∑ k, lowerUnit entries k i * D k * lowerUnit entries k j) :
    (realMatrix Z).PosDef := by
…

Mentions: OAI.MUB6.Certificate.lowerUnit, OAI.MUB6.Certificate.realMatrix