OAI/Combinatorics/Progressions/Estimates/AllocatedChosenFunctionalCoarsening.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedRefinedSiteReference line 66
2. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_site_expansion line 98
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_coarse_site_comparison line 203
4. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_normalized_coarse_comparison line 321
5. def OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceFunctional line 452
6. def OAI.Erdos3.VectorPolynomial.allocatedRefinedSiteFunctional line 527
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_accuracy_coarse_comparison line 584
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_normalized_reference_comparison line 756
9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_chosen_functional_coarsening line 967