OAI/Probability/BinarySweep/Trajectories/PathMomentMixed.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Sparse.centeredLineMoment_mixed line 16
2. theorem OAI.BinaryCoordinateSweeps.Sparse.occurrenceMoment_mixed line 35
3. theorem OAI.BinaryCoordinateSweeps.Sparse.pathMoment_mixed line 58
4. def OAI.BinaryCoordinateSweeps.endpointPathPolynomial line 116
5. def OAI.BinaryCoordinateSweeps.vertexIsolated line 119
6. lemma OAI.BinaryCoordinateSweeps.endpointValid_union_isolated line 124
7. lemma OAI.BinaryCoordinateSweeps.endpoint_subset_polynomial line 134
8. lemma OAI.BinaryCoordinateSweeps.centeredEndpointKernel_scaled line 148
9. theorem OAI.BinaryCoordinateSweeps.centeredEndpointKernel_good_expansion line 158