OAI/Analysis/Laughlin/Pair/HomogeneousCube.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.homogeneousEval_cube line 9
2. theorem OAI.Laughlin.homogeneousEval_linear line 17
3. theorem OAI.Laughlin.linear_natDegree line 24
4. def OAI.Laughlin.pairPartialPolynomial line 31
5. theorem OAI.Laughlin.pairPartialPolynomial_expansion line 37
6. theorem OAI.Laughlin.pairPartialPolynomial_degree line 53
7. theorem OAI.Laughlin.pairAffinePolynomial_degree line 64
8. theorem OAI.Laughlin.pairPartialPolynomial_cube line 73