OAI/Combinatorics/Progressions/Sampling/AllocatedClippedFullGridGlobal.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteValues line 33
  2. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteApproximation line 37
  3. def OAI.Erdos3.VectorPolynomial.allocatedFullGridNaturalVolume line 43
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridNaturalVolume_pos line 48
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteApproximation_error line 56
  6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_grid_site_approximation line 93
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridNaturalVolume_le_exp line 146
  8. def OAI.Erdos3.VectorPolynomial.allocatedFullGridCoefficientLog line 212
  9. def OAI.Erdos3.VectorPolynomial.allocatedFullGridWindowLog line 214
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridCoefficientLog_nonneg line 217
  11. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow line 237
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_integer line 245
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_nonempty line 255
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridCoefficientLog_sites line 268
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_card line 281
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_volume line 304
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridPhysicalCoefficient_bound line 331
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_zero line 357
  19. def OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedFullGridDensity line 430
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedFullGridDensity_mean line 435
  21. def OAI.Erdos3.VectorPolynomial.allocatedSlicedGridPhysicalVolume line 455
  22. def OAI.Erdos3.VectorPolynomial.allocatedSlicedGridSiteApproximation line 458
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedGridSiteApproximation_error line 464
  24. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSelectedApproximation line 532
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSelected_mass_eq line 544
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSelected_error line 558
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSelected_zero line 570
  28. def OAI.Erdos3.VectorPolynomial.allocatedFullGridPointTolerance line 596
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridPointTolerance_pos line 599
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridPointTolerance_inv line 602
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridWindowLog_nonneg line 610
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteWindow_error_budget line 635
  33. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteProfile line 687
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteProfile_measurable line 711
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteProfile_error line 720
  36. def OAI.Erdos3.VectorPolynomial.allocatedFullGridRowsOfMixed line 762
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridRowsOfMixed_integer line 767
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteValues_mixed line 779
  39. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteApproximation_mixed line 789
  40. def OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteChartPrefactor line 823
  41. theorem OAI.Erdos3.VectorPolynomial.allocatedFullGridSiteProfile_mixed line 827
  42. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridSiteProfile line 899
  43. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridPrefactor line 903
  44. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridSiteProfile_mixed line 906
  45. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridSiteProfile_measurable line 917
  46. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridPrefactor_support line 924
  47. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridSiteProfile_zero line 946
  48. def OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridGlobalPrefactor line 1004
  49. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridGlobalPrefactor_apply line 1009
  50. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridGlobalPrefactor_zero line 1014
  51. theorem OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridGlobalPrefactor_measurable line 1021