OAI/Combinatorics/SquareDifference/ExceptionalBasics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.tupleExceptionalLaw_marginal line 13
2. lemma OAI.SquareDifference.tensorLaw_weighted_marginal line 20
3. lemma OAI.SquareDifference.weighted_uniform_multilinear_crude line 49
4. def OAI.SquareDifference.exceptionalProduct line 77
5. def OAI.SquareDifference.actualMixedLaw line 79
6. lemma OAI.SquareDifference.exceptionalProduct_nonneg line 82
7. lemma OAI.SquareDifference.actualMixedLaw_nonneg line 88
8. lemma OAI.SquareDifference.actualMixedLaw_marginal line 91
9. lemma OAI.SquareDifference.actualMixedLaw_mass line 101
10. lemma OAI.SquareDifference.actualMixedLaw_crude line 106