OAI/Probability/BinarySweep/SparseBounds/SparseKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.centeredEndpointKernel line 16
2. lemma OAI.BinaryCoordinateSweeps.centeredEndpointKernel_isolated line 21
3. def OAI.BinaryCoordinateSweeps.pathEndpoints line 33
4. lemma OAI.BinaryCoordinateSweeps.endpointLine_path line 36
5. def OAI.BinaryCoordinateSweeps.shareLine line 41
6. lemma OAI.BinaryCoordinateSweeps.shareLine_symmetric line 44
7. lemma OAI.BinaryCoordinateSweeps.shareLine_probability line 50
8. lemma OAI.BinaryCoordinateSweeps.centeredEndpointKernel_support line 61
9. theorem OAI.BinaryCoordinateSweeps.centeredEndpointKernel_exceptional_probability line 77