OAI/Combinatorics/BooleanFunctions/Switching.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SquareRootDegree.Switching.EventSpace line 17
2. abbrev OAI.SquareRootDegree.Switching.FullSpace line 18
3. def OAI.SquareRootDegree.Switching.oldSum line 20
4. def OAI.SquareRootDegree.Switching.totalSum line 21
5. def OAI.SquareRootDegree.Switching.oldLabels line 22
6. def OAI.SquareRootDegree.Switching.observation line 24
7. def OAI.SquareRootDegree.Switching.predictor line 27
8. theorem OAI.SquareRootDegree.Switching.average_prod_add_sq line 31
9. theorem OAI.SquareRootDegree.Switching.oldSum_zero line 41
10. theorem OAI.SquareRootDegree.Switching.oldSum_sq line 52
11. theorem OAI.SquareRootDegree.Switching.totalSum_sq line 68
12. theorem OAI.SquareRootDegree.Switching.prediction_error line 76
13. theorem OAI.SquareRootDegree.Switching.retained_gain line 106
14. abbrev OAI.SquareRootDegree.Switching.Slots line 123
15. def OAI.SquareRootDegree.Switching.fullEquiv line 125
16. theorem OAI.SquareRootDegree.Switching.sum_full line 135
17. theorem OAI.SquareRootDegree.Switching.full_conditional_sum line 148