OAI/Combinatorics/Progressions/Estimates/AllocatedIdealPhysicalCover.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_cover_site_factor line 27
  2. theorem OAI.Erdos3.lipschitz_complex_div_two line 104
  3. theorem OAI.Erdos3.complex_div_two_norm_le line 117
  4. theorem OAI.Erdos3.two_scaled_product_identity line 122
  5. def OAI.Erdos3.coverSiteCoefficient line 131
  6. theorem OAI.Erdos3.coverSiteCoefficient_bound line 135
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_cover_site_expansion line 158
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_normalized_cover_site_expansion line 226
  9. def OAI.Erdos3.VectorPolynomial.activeAmbientAxisDecidableEq line 313
  10. def OAI.Erdos3.VectorPolynomial.allocatedActiveAmbientPoint line 329
  11. def OAI.Erdos3.VectorPolynomial.allocatedActiveAmbientSum line 336
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveAmbientPoint_chart line 343
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveAmbientSum_chart line 352
  14. def OAI.Erdos3.VectorPolynomial.ActiveAmbientRepresentation line 363
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_ambient_representation line 373
  16. def OAI.Erdos3.VectorPolynomial.ActiveAmbientProfileRepresentation line 402
  17. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_ambient_profile line 414
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_window_cover_profile line 486
  19. def OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor line 597
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_apply line 605
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_zero line 615
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_measurable line 620
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteProfile_zero_outside line 629
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_cover_profile line 682
  25. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_ideal_physical_cover line 798