OAI/Combinatorics/Progressions/Estimates/AllocatedTestUniformCoarseJointStatement.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformActualTupleStatement line 15
2. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformActualScalarTupleStatement line 156
3. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformActualNormalizedTupleStatement line 308
4. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformSpatiallyNormalizedTupleStatement line 469
5. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformBudgetedTupleStatement line 630
6. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformChosenScaleTupleStatement line 785
7. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformOriginalChosenTupleStatement line 923
8. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformCenteredChosenTupleStatement line 1058
9. theorem OAI.Erdos3.VectorPolynomial.allocatedTestUniformActualTupleComparison line 1210
10. def OAI.Erdos3.VectorPolynomial.allocatedTestUniformCoarseJointStatement line 1277