AuxiliaryInterpretation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Interpreting the certificate's expanded auxiliary functions

The integer tagged terms are ordinary finite linear combinations of the manuscript's two auxiliary functions. Their real Gram products expand into the exact mixed-moment expressions used by the certificate. Positive semidefiniteness of a coefficient matrix proves nonnegativity independently of how its entries or its finite lists of terms were obtained.

def OAI.MUB6.Certificate.GramFunctions.LinearForm.auxiliaryEval line 21
def OAI.MUB6.Certificate.GramFunctions.LinearForm.mixedGram line 25
Source documentation
Explicit mixed-moment expansion of a pair of integer linear forms.
```
def LinearForm.mixedGram (P Q : LinearForm) (B : Fin 7 → Basis) : ℝ :=
…
```
Mentions: OAI.MUB6.Certificate.GramFunctions.LinearForm, OAI.MUB6.Basis
theorem OAI.MUB6.Certificate.GramFunctions.LinearForm.auxiliaryEval_gram line 30
theorem OAI.MUB6.Certificate.GramFunctions.LinearForm.mixedGram_psd_nonneg line 41
Source documentation
A positive semidefinite matrix proves nonnegativity of the fully expanded mixed expression for any finite family of integer linear forms.
```
theorem LinearForm.mixedGram_psd_nonneg {ι : Type*} [Fintype ι] [DecidableEq ι]
    (P : ι → LinearForm) (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (Z : Matrix ι ι ℝ) (hZ : Z.PosSemidef) :
    0 ≤ ∑ i, ∑ j, Z i j * (P i).mixedGram (P j) B := by
…
```
Mentions: OAI.MUB6.Certificate.GramFunctions.LinearForm, OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Certificate.GramFunctions.LinearForm.mixedGram