OAI/Combinatorics/Progressions/Estimates/AllocatedProductSourceCover.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSource_fixed line 53
2. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredResidueWeight_test_mul line 111
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_test_mask line 123
4. theorem OAI.Erdos3.VectorPolynomial.allocated_product_recentered_primitive_comparison line 174
5. theorem OAI.Erdos3.VectorPolynomial.allocated_product_recentered_separated_comparison line 358
6. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_primitive_comparison line 543
7. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_bounded_comparison line 736
8. theorem OAI.Erdos3.VectorPolynomial.allocated_product_original_exponential_comparison_mesh line 944
9. theorem OAI.Erdos3.VectorPolynomial.allocated_product_ideal_exponential_comparison line 1137
10. theorem OAI.Erdos3.VectorPolynomial.allocated_product_source_exponential_comparison line 1306