OAI/Probability/BinarySweep/SparseBounds/SparseAmplitude.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.placementProbability_uniform_bound line 17
2. lemma OAI.BinaryCoordinateSweeps.endpointProbability_scaled_bound line 44
3. lemma OAI.BinaryCoordinateSweeps.alternatingSubsetSum_abs_le line 60
4. theorem OAI.BinaryCoordinateSweeps.centeredEndpointKernel_amplitude line 75
5. lemma OAI.BinaryCoordinateSweeps.Sparse.productProbability_uniform line 103
6. lemma OAI.BinaryCoordinateSweeps.Sparse.sum_injective_le line 108
7. theorem OAI.BinaryCoordinateSweeps.Sparse.sum_square_le_uniform_event line 115
8. def OAI.BinaryCoordinateSweeps.placementEndpointArray line 157
9. lemma OAI.BinaryCoordinateSweeps.placementEndpointArray_injective line 160
10. theorem OAI.BinaryCoordinateSweeps.centeredEndpointKernel_hs_bound line 172