OAI/Combinatorics/Progressions/Sampling/AllocatedUniformGridVolumeCap.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_full_site_support line 47
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_integer_rows line 75
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_grid_natural_bound line 101
  4. def OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRadius line 178
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRadius_nonneg line 183
  6. def OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRowWindow line 188
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRowWindow_card_le line 198
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRowWindow_measurable line 212
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRowWindow_measure_lt_top line 222
  10. def OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRegion line 233
  11. def OAI.Erdos3.VectorPolynomial.allocatedCutoffGridVolumeCap line 236
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRegion_measurable line 240
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRegion_measure_lt_top line 245
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRegion_measure_le line 252
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridRegion_mem_of_bound line 278
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_mem_gridRegion line 290
  17. def OAI.Erdos3.VectorPolynomial.allocatedCutoffGridEnvelope line 299
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridEnvelope_nonneg line 305
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridEnvelope_measurable line 312
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridEnvelope_integrable line 317
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridEnvelope_integral_le line 324
  22. def OAI.Erdos3.VectorPolynomial.allocatedUniformGridVolumeCap line 359
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformGridVolumeCap_one_le line 364
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffGridVolumeCap_le_uniform line 374