OAI/Combinatorics/Progressions/Lattices/AllocatedAffineRecenteredSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_l1 line 96
2. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_l1_small line 211
3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_l1_of_length line 426
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAffineIdeal_l1_reference line 586
5. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_sampled_l1_of_length line 761
6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIdeal_recentered_source_of_length line 968