OAI/Combinatorics/Progressions/Estimates/PreparedModularCanonicalDetectorPositive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_native_source_with_bounds line 12
2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_prepared_source line 155
3. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_initial_source line 304
4. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_narrow_width_le_one line 415
5. def OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorConstructedInterface line 489
6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector line 583
7. def OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorPositiveInterface line 894
8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_positive line 989