OAI/Combinatorics/Progressions/Sampling/AllocatedFullGridCoefficientBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedFullGridPrimitiveResourceLog line 10
2. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridPrimitiveResourceLog_nonneg line 16
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFullGridPrimitiveResourceLog_bound line 26
4. theorem OAI.Erdos3.VectorPolynomial.allocated_full_grid_primitive_error line 78
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_grid_primitive_error line 187
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_grid_primitive_sampling line 331
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_grid_primitive_comparison line 380
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_early_full_grid_family line 522
9. def OAI.Erdos3.VectorPolynomial.allocatedFullGridCoefficientPreLog line 591
10. theorem OAI.Erdos3.VectorPolynomial.coverSiteCoefficient_uniform_exp_bound line 594
11. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGrid_coefficient_pre_bound line 622