Exact positive semidefinite certificate calculus

Integer fraction-free Schur certificates are checked by the Lean kernel.

def PersistentSOS.quadraticForm {n : ℕ} (A : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

The quadratic form of a real matrix.

Equations

• PersistentSOS.quadraticForm A x = ∑ i : Fin n, ∑ j : Fin n, x i * A i j * x j

def PersistentSOS.IsPSD {n : ℕ} (A : Fin n → Fin n → ℝ) : Prop

Nonnegativity of the quadratic form; symmetry is verified independently.

Equations

• PersistentSOS.IsPSD A = ∀ (x : Fin n → ℝ), 0 ≤ PersistentSOS.quadraticForm A x

theorem PersistentSOS.quadraticForm_zero (A : Fin 0 → Fin 0 → ℝ) : IsPSD A

theorem PersistentSOS.schur_step {n : ℕ} (A : Fin (n + 1) → Fin (n + 1) → ℝ) (B : Fin n → Fin n → ℝ) (p : ℝ) (hp : 0 < p) (ha : 0 < A 0 0) (hsym : ∀ (i : Fin n), A i.succ 0 = A 0 i.succ) (hstep : ∀ (i j : Fin n), p * B i j = A 0 0 * A i.succ j.succ - A i.succ 0 * A 0 j.succ) (hB : IsPSD B) : IsPSD A

One fraction - free Schur step, with an independently checked previous pivot.

theorem PersistentSOS.integer_schur_step {n : ℕ} (A : Fin (n + 1) → Fin (n + 1) → ℤ) (B : Fin n → Fin n → ℤ) (p : ℤ) (hp : 0 < p) (ha : 0 < A 0 0) (hsym : ∀ (i : Fin n), A i.succ 0 = A 0 i.succ) (hstep : ∀ (i j : Fin n), p * B i j = A 0 0 * A i.succ j.succ - A i.succ 0 * A 0 j.succ) (hB : IsPSD fun (i j : Fin n) => ↑(B i j)) : IsPSD fun (i j : Fin (n + 1)) => ↑(A i j)

Integer identities suffice for a Schur step over the reals.