OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorProductive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductivity_le_budget line 11
2. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductivity_physical_bounds line 19
3. def OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductivityExponent line 50
4. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductivityExponent_two_le line 53
5. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneral_productivity_bounds line 57
6. def OAI.Erdos3.VectorPolynomial.PreparedModularGeneralProductiveInterface line 247
7. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductiveInterface_of_bounds line 339
8. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductiveInterface_of_width_bounds line 458
9. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralDetectorProductive line 508