OAI/Combinatorics/Progressions/Dynamics/AllocatedIdealCoverErrorBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedSiteConstructionLog line 14
2. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteConstructionLog_bounds line 21
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSiteConstructionLog_bound line 36
4. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteWindow_primitive_bounds line 53
5. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteConstruction_primitive_budget line 74
6. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverErrorLog line 125
7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverErrorLog_controls line 132
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedIdealCoverErrorLog_bound line 150