OAI/Combinatorics/Progressions/Probability/AllocatedSlicedProxyLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedOneCube_uniform_density_comparison line 30
2. def OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetDensity line 106
3. def OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy line 110
4. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetDensity_measurable line 117
5. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetDensity_probability line 129
6. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetMap_measurable line 136
7. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_image_law line 150
8. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_probability line 166
9. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_endpoint_test line 176