OAI/Combinatorics/Progressions/Estimates/AllocatedFiniteCoefficientL1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_residue_coefficient_comparison line 28
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalLongJetTarget_measurable line 157
3. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteLongJetProxy_measurable line 171
4. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetTarget_principal_product_zero line 182
5. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteLongJet_l1_comparison line 199