OAI/Combinatorics/Progressions/Estimates/AllocatedFullAmbientSiteFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.fullSitePlateauFactor line 13
2. theorem OAI.Erdos3.fullSitePlateauFactor_norm_le line 16
3. theorem OAI.Erdos3.fullSitePlateauFactor_lipschitz line 22
4. theorem OAI.Erdos3.fullSitePlateauFactor_eq line 38
5. theorem OAI.Erdos3.fullSitePlateauFactor_nonzero_box line 42
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_ambient_site_factor line 64
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_full_buffered_ambient_site_factor line 81
8. theorem OAI.Erdos3.VectorPolynomial.allocatedFullAmbientSiteFactor_chart line 96
9. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSitePlateau_point_bound line 113
10. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSitePlateau_nonzero_mem_quarter line 125