OAI/Combinatorics/Progressions/Dynamics/PreparedModularCanonicalDetectorPeriodBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_canonicalSlicedModelPrefactor_budget line 12
2. theorem OAI.Erdos3.VectorPolynomial.exists_canonicalSlicedPeriod_common_budget line 70
3. theorem OAI.Erdos3.VectorPolynomial.exists_detectedCanonical_common_grid_budget line 186
4. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_period_budget line 243
5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_grid_parameters line 359
6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_common_grid_budget line 408