OAI/Probability/BinarySweep/FiniteLaws/LightLineBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_le_two_pow line 14
2. lemma OAI.BinaryCoordinateSweeps.Sparse.light_real_lt line 31
3. theorem OAI.BinaryCoordinateSweeps.Sparse.centeredLineMoment_light line 36
4. def OAI.BinaryCoordinateSweeps.Sparse.multilineMoment line 126
5. lemma OAI.BinaryCoordinateSweeps.Sparse.multilineMoment_monomial line 130
6. lemma OAI.BinaryCoordinateSweeps.Sparse.multiline_prod_X line 135
7. theorem OAI.BinaryCoordinateSweeps.Sparse.multilineMoment_factor line 148
8. lemma OAI.BinaryCoordinateSweeps.Sparse.multilineMoment_centered line 169