OAI/Probability/BinarySweep/GridBounds/GroupedTypes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Signed.groupOf line 18
2. def OAI.BinaryCoordinateSweeps.Signed.groupedProjection line 21
3. lemma OAI.BinaryCoordinateSweeps.Signed.groupedProjection_psd line 26
4. lemma OAI.BinaryCoordinateSweeps.Signed.groupedProjection_idempotent line 32
5. lemma OAI.BinaryCoordinateSweeps.Signed.groupedProjection_commutes line 39
6. lemma OAI.BinaryCoordinateSweeps.Signed.grouped_density_domination line 48
7. lemma OAI.BinaryCoordinateSweeps.Signed.grouped_density_card_bound line 64