OAI/Combinatorics/Progressions/Lattices/AllocatedAffineFiniteModelL2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdeal_measurable line 24
2. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdeal_coordinate_support line 33
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdeal_normalized_cap line 50
4. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineRowIdeal_cutoff_fixes line 109
5. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineRowIdeal_cutoff_fixes_mean line 129
6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineProductPrefactor_cap line 219
7. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineFiniteModel_comparison line 333
8. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineFiniteModel_l1 line 511
9. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineFiniteModel_l2 line 718