OAI/Combinatorics/Progressions/Estimates/AllocatedTrimmedVectorSite.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalRootBudget line 23
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalRootBudget_nonneg line 26
  3. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalEntryBudget line 30
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalEntryBudget_one_le line 33
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_directions_bound line 39
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_root_bound line 56
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_root_sum line 76
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_root_budget line 85
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_root_entry_bound line 92
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_direction_entry_bound line 99
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_kernel_range line 107
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_period line 115
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_minor line 123
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_good_kernel line 131
  15. theorem OAI.Erdos3.anisotropicSpatialError_nonneg line 151
  16. theorem OAI.Erdos3.canonicalVectorSpatialSiteApprox_error line 159
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_direction_sum line 237
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_window_bound line 246
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterSite_bound line 283
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterSite_sum_bound line 296
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_nonempty line 303
  22. def OAI.Erdos3.VectorPolynomial.allocatedPrimitiveRootRatio line 321
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedPrimitiveRootRatio_bounds line 323
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalRootBudget_zero line 342
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalRootBudget_zero_ratio line 347
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_kernel_error line 385
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_vector_site_error line 461