OAI/Probability/BinarySweep/Trajectories/EndpointEntryBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_abs_le line 15
2. lemma OAI.BinaryCoordinateSweeps.occurrences_injective_le line 27
3. lemma OAI.BinaryCoordinateSweeps.endpoint_mixed_occurrences_le line 35
4. def OAI.BinaryCoordinateSweeps.endpointLight line 63
5. lemma OAI.BinaryCoordinateSweeps.endpoint_pathMoment_bound line 67
6. theorem OAI.BinaryCoordinateSweeps.centeredEndpointKernel_good_bound line 118