OAI/Combinatorics/Progressions/Estimates/AllocatedMaskedCoefficientSampleAE.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_sample line 25
2. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_sample_event line 54
3. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_event_of_nonzero line 104
4. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_event line 132
5. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_affine_event line 158
6. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_sample_ae line 197