OAI/Combinatorics/BooleanFunctions/Readout.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SquareRootDegree.Observations.singletonSum_eq_average line 17
2. def OAI.SquareRootDegree.Observations.readSign line 31
3. theorem OAI.SquareRootDegree.Observations.readSign_boolean line 33
4. theorem OAI.SquareRootDegree.Observations.readSign_mul line 37
5. def OAI.SquareRootDegree.Observations.readout line 43
6. theorem OAI.SquareRootDegree.Observations.readout_boolean line 46
7. theorem OAI.SquareRootDegree.Observations.readout_degree line 49
8. theorem OAI.SquareRootDegree.Observations.readout_sum line 55
9. theorem OAI.SquareRootDegree.Observations.exists_readout line 65
10. def OAI.SquareRootDegree.Observations.cubeReindex line 95
11. theorem OAI.SquareRootDegree.Observations.cubeSum_reindex line 102
12. theorem OAI.SquareRootDegree.Observations.singletonSum_reindex line 106
13. theorem OAI.SquareRootDegree.Observations.nonconstant_of_singletonSum_pos line 118
14. theorem OAI.SquareRootDegree.Observations.positive_card_of_nonconstant line 127
15. theorem OAI.SquareRootDegree.Observations.reindex_violation line 136
16. theorem OAI.SquareRootDegree.Observations.sqrt_ratio_bound line 158
17. theorem OAI.SquareRootDegree.Observations.violation_of_observation line 180