OAI/Probability/BinarySweep/SparseBounds/FewSparse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinaryCoordinateSweeps.centeredEndpointHS_few_sparse line 20
2. theorem OAI.BinaryCoordinateSweeps.conditional_specht_few_sparse line 55
3. lemma OAI.BinaryCoordinateSweeps.sparse_tail_le_quarter line 69
4. lemma OAI.BinaryCoordinateSweeps.few_sparse_sign_geometry line 81
5. lemma OAI.BinaryCoordinateSweeps.many_sparse_sign_geometry line 98
6. instance OAI.BinaryCoordinateSweeps.finitePathFamily line 119
7. def OAI.BinaryCoordinateSweeps.sparseEndpointBound line 127
8. lemma OAI.BinaryCoordinateSweeps.sparseEndpointBound_eventually line 133
9. theorem OAI.BinaryCoordinateSweeps.sparse_finite_radius line 157