OAI/Combinatorics/PolynomialVacuum/Puncture/Gram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumCylinder.evenMomentEvaluation line 8
2. theorem OAI.PolynomialVacuumCylinder.evenMomentEvaluation_expand line 11
3. theorem OAI.PolynomialVacuumCylinder.evenMomentEvaluation_integrable line 24
4. theorem OAI.PolynomialVacuumCylinder.denominator_gram_identity line 31
5. theorem OAI.PolynomialVacuumCylinder.evenMomentEvaluation_nonzero line 47
6. theorem OAI.PolynomialVacuumCylinder.denominator_gram_pos line 69
7. theorem OAI.PolynomialVacuumCylinder.denominatorMomentMatrix_posDef line 92
8. theorem OAI.PolynomialVacuumCylinder.denominatorMomentMatrix_det_pos line 102