OAI/Combinatorics/Progressions/Estimates/AllocatedUnitSiteFactors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_ambient_site_factor line 23
2. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientSiteFactor_chart line 40
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_unit_ambient_site_factor line 76
4. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTerm_ambient_factorization line 132
5. theorem OAI.Erdos3.BooleanCubeKernel.allocatedCoveredSiteTerm_physical_ambient_factorization line 225
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTerm_unit_ambient_factorization line 290
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_unit_site_family line 317
8. theorem OAI.Erdos3.BooleanCubeKernel.exists_allocated_physical_lipschitz_site_factors line 365
9. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTerm_unit_factorization line 436
10. theorem OAI.Erdos3.BooleanCubeKernel.exists_allocated_physical_unit_site_factors line 492