OAI/Combinatorics/Progressions/Estimates/AllocatedProductSeparatedRawData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedProductCoarse_error_bound line 13
2. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_separated_comparison line 91
3. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_separated_bounded_comparison line 285
4. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_separated_exponential_mesh line 494
5. theorem OAI.Erdos3.VectorPolynomial.allocated_product_ideal_separated_exponential_comparison line 688
6. theorem OAI.Erdos3.VectorPolynomial.allocated_product_source_separated_exponential_comparison line 858
7. theorem OAI.Erdos3.VectorPolynomial.allocated_product_primitive_coarse_comparison line 1028
8. def OAI.Erdos3.VectorPolynomial.AllocatedProductSeparatedContract line 1218
9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSeparatedContract_of_sampling line 1312
10. def OAI.Erdos3.VectorPolynomial.AllocatedProductSeparatedRawData line 1368