OAI/Probability/BinarySweep/Trajectories/SparseOccupancy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinaryCoordinateSweeps.Sparse.occupancy_probability_le line 12
2. def OAI.BinaryCoordinateSweeps.Sparse.smallSetEncode line 43
3. lemma OAI.BinaryCoordinateSweeps.Sparse.smallSetEncode_mem line 48
4. lemma OAI.BinaryCoordinateSweeps.Sparse.smallSetEncode_injective line 65
5. lemma OAI.BinaryCoordinateSweeps.Sparse.smallSet_card_bound line 72
6. theorem OAI.BinaryCoordinateSweeps.Sparse.line_sets_occupancy_probability_le line 77