OAI/Combinatorics/Progressions/Geometry/AllocatedFullSiteSupport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedFullMixedSiteValue line 21
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedFullMixedSiteValue_projection line 26
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedFullMixedSiteValue_continuous line 34
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedFullMixedSiteValue_point_bound line 44
  5. def OAI.Erdos3.VectorPolynomial.allocatedIdealSiteChartFactor line 95
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteChartFactor_norm_le line 101
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteChartFactor_apply line 119
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteChartFactor_product line 133
  9. def OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor line 161
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor_norm_le line 166
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor_continuous line 171
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor_eq line 177
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor_nonzero_point_bound line 185
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedMixedSiteFactor_nonzero_mem_quarter line 198
  15. def OAI.Erdos3.VectorPolynomial.allocatedFullAmbientSiteCoordinates line 238
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFullAmbientSiteCoordinates_point line 244
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFullAmbientSiteCoordinates_lipschitz line 263
  18. def OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor line 331
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_norm_le line 336
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_measurable line 344
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_enlarge line 358
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_apply line 379
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_product line 395
  24. def OAI.Erdos3.VectorPolynomial.singleSiteFromLayered line 418
  25. theorem OAI.Erdos3.VectorPolynomial.singleSiteFromLayered_lipschitz line 421
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedFullAmbientSiteCoordinates_layered_point line 435
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBox_full_site_bound line 473