OAI/Combinatorics/Progressions/Estimates/PreparedModularCanonicalDetectorPositiveBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.preparedResource_nonneg line 12
  2. theorem OAI.Erdos3.VectorPolynomial.prepared_slicedGridGeometryLog_mono line 19

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorNativeBounds.lean:225 (same declaration text).

  3. theorem OAI.Erdos3.VectorPolynomial.prepared_affineAmbientPrimitiveBudget_mono line 27

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorNativeBounds.lean:233 (same declaration text).

  4. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_ideal_site_bound line 36
  5. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_ambient_bound line 54
  6. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_grid_bound line 84
  7. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_grid_resource_width_bound line 114
  8. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_native_inputs line 143
  9. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_final_error_bound line 164
  10. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_native_budget_mono line 175
  11. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_required_bounds line 187
  12. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_positive_bounds line 232