OAI/Combinatorics/PolynomialVacuum/Puncture/Reference.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PolynomialVacuumCylinder.denominatorReferenceWeight_leline 9 - theorem
OAI.PolynomialVacuumCylinder.denominatorReferenceWeight_measurableline 16 - theorem
OAI.PolynomialVacuumCylinder.denominator_reference_moment_integrableline 20 - theorem
OAI.PolynomialVacuumCylinder.denominatorReferenceMatrix_entry_integrableline 29 - theorem
OAI.PolynomialVacuumCylinder.denominatorCorrection_le_oneline 34 - theorem
OAI.PolynomialVacuumCylinder.denominatorCorrectionMatrix_entry_integrableline 40 - theorem
OAI.PolynomialVacuumCylinder.referenceEvaluation_expandline 55 - theorem
OAI.PolynomialVacuumCylinder.referenceEvaluation_integrableline 68 - theorem
OAI.PolynomialVacuumCylinder.denominator_reference_gram_identityline 75 - theorem
OAI.PolynomialVacuumCylinder.denominatorReferenceMatrix_posDefline 91 - theorem
OAI.PolynomialVacuumCylinder.denominatorReferenceMatrix_det_posline 110