OAI/Combinatorics/Progressions/Probability/AllocatedRefinedCoefficientMass.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.finiteTripleCoefficientMass_le line 16
2. def OAI.Erdos3.VectorPolynomial.allocatedConstructedSpatialCoefficientAt line 69
3. theorem OAI.Erdos3.VectorPolynomial.allocatedConstructedSpatialCoefficient_pre_bound line 82
4. theorem OAI.Erdos3.VectorPolynomial.allocatedConstructedSpatialCoefficient_coarse_bound line 209
5. theorem OAI.Erdos3.VectorPolynomial.finiteRepeatedCoefficientMass_le line 299
6. theorem OAI.Erdos3.VectorPolynomial.finiteGridRepeatedCoefficientMass_le line 313
7. def OAI.Erdos3.VectorPolynomial.allocatedRefinedConstructedSpatialCoefficientAt line 371
8. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedConstructedSpatialCoefficientAt_le line 386
9. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedConstructedSpatialCoefficient_pre_bound line 424