OAI/Combinatorics/Progressions/Estimates/AllocatedPeriodicAmbientSiteExpansion.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGrid_normalized_norm_le line 39
  2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_scalar_site_expansion line 73
  3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_joint_site_expansion line 165
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteApproximation_error line 271
  5. def OAI.Erdos3.VectorPolynomial.allocatedActiveSiteBounds line 328
  6. def OAI.Erdos3.VectorPolynomial.allocatedGridRowFromIntegerValues line 368
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedGridIntegerValues_fromValues line 375
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedGridRowFromIntegerValues_inverse line 382
  9. def OAI.Erdos3.VectorPolynomial.allocatedActiveRowsFromSites line 389
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteValues_rowsFromSites line 394
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteApproximation_rowsFromSites line 402
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteApproximation_affine line 411
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_periodic_ambient_site_factor line 452
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPeriodicAmbientSiteFactor_chart line 492
  15. theorem OAI.Erdos3.lipschitz_complex_div_four line 532
  16. theorem OAI.Erdos3.complex_div_four_norm_le line 545
  17. theorem OAI.Erdos3.four_scaled_product_identity line 550
  18. def OAI.Erdos3.periodicAmbientSiteCoefficient line 559
  19. theorem OAI.Erdos3.periodicAmbientSiteCoefficient_bound line 563
  20. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_periodic_ambient_site_expansion line 587