OAI/Combinatorics/BooleanFunctions/Observations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SquareRootDegree.Observations.cubeSum line 18
2. def OAI.SquareRootDegree.Observations.score line 19
3. def OAI.SquareRootDegree.Observations.variance line 20
4. theorem OAI.SquareRootDegree.Observations.cubeSum_zero line 23
5. theorem OAI.SquareRootDegree.Observations.score_zero line 36
6. theorem OAI.SquareRootDegree.Observations.cubeSum_block line 41
7. def OAI.SquareRootDegree.Observations.grouped line 45
8. theorem OAI.SquareRootDegree.Observations.grouped_degree line 49
9. theorem OAI.SquareRootDegree.Observations.grouped_score line 62
10. theorem OAI.SquareRootDegree.Observations.variance_nonneg line 85
11. def OAI.SquareRootDegree.Observations.standardValue line 88
12. def OAI.SquareRootDegree.Observations.standard line 91
13. theorem OAI.SquareRootDegree.Observations.standard_zero line 94
14. theorem OAI.SquareRootDegree.Observations.standard_sq line 99