OAI/Probability/BinarySweep/GridBounds/GridLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.gridLaw line 15
2. lemma OAI.BinaryCoordinateSweeps.pushLaw_inverse line 18
3. lemma OAI.BinaryCoordinateSweeps.pushLaw_injective line 24
4. lemma OAI.BinaryCoordinateSweeps.binary_splitLaw line 30
5. lemma OAI.BinaryCoordinateSweeps.grid_splitLaw line 50
6. lemma OAI.BinaryCoordinateSweeps.oneAxis_gridLaw line 67
7. theorem OAI.BinaryCoordinateSweeps.gridLaw_binary line 82