OAI/Combinatorics/Progressions/Estimates/AllocatedSiteBufferLog.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCutoff_mul line 24
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCutoff_complex_mul line 48
  3. def OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope line 84
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope_nonneg line 89
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealNormalizedJets_bound_of_sites line 96
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteApproximation_envelope line 110
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteApproximation_error line 167
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_measurable line 238
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteSupport_measurable line 252
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope_measurable line 264
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope_le_box line 269
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_ideal_site_approximation line 308
  13. def OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer line 390
  14. def OAI.Erdos3.VectorPolynomial.allocatedSiteBufferLip line 393
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_range line 397
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_abs_le line 403
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_measurable line 409
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_lipschitz line 415
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_support line 430
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope_le_buffer line 440
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_cap_le_exp line 480
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteBuffer_lip_le_exp line 488