OAI/Combinatorics/Progressions/Estimates/AllocatedSiteWindowLogBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedSiteAxisWindowLog line 11
2. def OAI.Erdos3.VectorPolynomial.allocatedSiteFamilyWindowLog line 14
3. def OAI.Erdos3.VectorPolynomial.allocatedSitePointToleranceLog line 17
4. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteAxisWindowLog_nonneg line 20
5. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteFamilyWindowLog_nonneg line 26
6. theorem OAI.Erdos3.VectorPolynomial.allocatedSitePointToleranceLog_nonneg line 32
7. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerAxes_card_le line 45
8. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteAxisWindowVolume_exp_bound line 52
9. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteFamilyWindowVolume_exp_bound line 63
10. theorem OAI.Erdos3.VectorPolynomial.allocatedSitePointTolerance_inverse_exp_bound line 77