OAI/Combinatorics/Progressions/Estimates/PreparedModularCanonicalDetectorAmbientConsumer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.preparedModularDetector_scalar_resource_bounds line 13
2. structure OAI.Erdos3.VectorPolynomial.PreparedModularDetectorAmbientBounds line 80
3. theorem OAI.Erdos3.VectorPolynomial.row_count_exp line 135
4. theorem OAI.Erdos3.VectorPolynomial.preparedModularDetector_ambient_bounds line 154
5. structure OAI.Erdos3.VectorPolynomial.PreparedModularGeneralEarlyAnalyticBounds line 291
6. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_early_analytic_bounds line 328
7. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_early_normalizer line 399
8. structure OAI.Erdos3.VectorPolynomial.PreparedModularGeneralLateAmbientBounds line 434
9. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_late_ambient_bounds line 456
10. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetectorAmbientConsumer line 607