OAI/Combinatorics/Progressions/Probability/AllocatedErrorSampledMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedMajorantRawDensity line 32
2. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorAmbientKernel_mixed_point line 39
3. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_chart line 62
4. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_lintegral line 90
5. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_mass_of_box line 143
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_mass line 206
7. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_integrable_mass line 224
8. theorem OAI.Erdos3.BooleanCubeKernel.exists_allocated_error_sampled_mass line 261