OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalExponentialCover.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocated_residue_site_reconstructed_comparison line 42
2. theorem OAI.Erdos3.VectorPolynomial.allocated_residue_site_reconstructed_primitive_comparison line 204
3. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedReference_recenter_supported line 411
4. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredResidueWeight line 470
5. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_residue_weight line 480
6. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredResidueWeight_norm_le line 497
7. theorem OAI.Erdos3.VectorPolynomial.allocated_recentered_primitive_comparison line 565
8. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_selected_mean line 741
9. theorem OAI.Erdos3.VectorPolynomial.allocated_original_primitive_comparison line 814
10. theorem OAI.Erdos3.VectorPolynomial.allocated_original_bounded_comparison line 1004
11. theorem OAI.Erdos3.VectorPolynomial.allocated_original_exponential_comparison line 1209