OAI/Combinatorics/Progressions/Estimates/AllocatedChosenOriginalIdealAt.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedFixedDataSourceAt line 58
2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedData_source_of_pointwise line 166
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleDifference_decomposition line 299
4. def OAI.Erdos3.VectorPolynomial.allocatedOriginalTupleDifference line 306
5. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalTupleDifference_bound line 316
6. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalTupleDifference_exp_bound line 326
7. def OAI.Erdos3.VectorPolynomial.AllocatedChosenOriginalIdealAt line 397