OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorNativeBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.generalDetectorCoefficientCost line 10
  2. def OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetectorResources line 13
  3. theorem OAI.Erdos3.VectorPolynomial.generalResources_map line 45
  4. theorem OAI.Erdos3.VectorPolynomial.generalResources_total_map line 54
  5. theorem OAI.Erdos3.VectorPolynomial.generalResources_bounds_of_list line 61
  6. theorem OAI.Erdos3.VectorPolynomial.natMv_eval_nonneg line 67
  7. theorem OAI.Erdos3.VectorPolynomial.natMv_eval_mono line 76
  8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralDetector_resource_budget line 87
  9. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetectorResources_nativeBudget_eq line 131
  10. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetectorResources_early_fields_eq line 137
  11. theorem OAI.Erdos3.VectorPolynomial.generalDetectorCoefficientCost_single line 145
  12. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetectorResources_primitive_domination line 152
  13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralDetector_early_native_budget line 192
  14. theorem OAI.Erdos3.VectorPolynomial.generalResource_nonneg line 218
  15. theorem OAI.Erdos3.VectorPolynomial.prepared_slicedGridGeometryLog_mono line 225

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedModularCanonicalDetectorPositiveBounds.lean:19 (same declaration text).

  16. theorem OAI.Erdos3.VectorPolynomial.prepared_affineAmbientPrimitiveBudget_mono line 233

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedModularCanonicalDetectorPositiveBounds.lean:27 (same declaration text).

  17. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_ideal_site_bound line 242
  18. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_ambient_bound line 259
  19. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_grid_bound line 289
  20. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_grid_resource_width_bound line 321
  21. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_native_inputs line 352
  22. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_final_error_bound line 373
  23. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_native_budget_mono line 384
  24. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_required_bounds line 396