OAI/Combinatorics/Progressions/Estimates/AllocatedPhysicalLongIdealCap.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientRadius line 21
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientRadius_nonneg line 26
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientRadius_physical line 30
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientRadius_sites line 34
  5. def OAI.Erdos3.VectorPolynomial.allocatedSiteAxisWindowVolume line 39
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteAxisWindowVolume_nonneg line 42
  7. def OAI.Erdos3.VectorPolynomial.allocatedSiteFamilyWindowVolume line 48
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteFamilyWindowVolume_nonneg line 52
  9. def OAI.Erdos3.VectorPolynomial.allocatedSitePointTolerance line 59
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedSitePointTolerance_spec line 62
  11. def OAI.Erdos3.VectorPolynomial.allocatedGridSiteWindow line 88
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGridSiteWindow_mem line 96
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedGridSiteWindow_integer line 105
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedGridSiteWindow_card_le line 114
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteWindow_volume line 128
  16. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverSupport line 169
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverSupport_nonneg line 175
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverSupport_inactive line 183
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverSupport_ideal line 193
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverSupport_window line 200
  21. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverRadius line 212
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverRadius_pos line 216
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveWindow_scaled_bound line 241
  24. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal line 294
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_measurable line 299
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_relative_support line 305
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_cover_support line 314
  28. def OAI.Erdos3.VectorPolynomial.allocatedIdealProfileLog line 333
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealProfileLog_nonneg line 336
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_exp_bound line 355
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_primitive_bound line 370