OAI/Probability/BinarySweep/FiniteLaws/OccurrenceMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Sparse.occurrences line 12
2. lemma OAI.BinaryCoordinateSweeps.Sparse.sum_occurrences line 14
3. lemma OAI.BinaryCoordinateSweeps.Sparse.prod_occurrences line 18
4. lemma OAI.BinaryCoordinateSweeps.Sparse.occurrenceMoment_eq line 23
5. theorem OAI.BinaryCoordinateSweeps.Sparse.occurrenceMoment_light line 35