OAI/Combinatorics/Progressions/Geometry/AllocatedPositiveSpatialComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_comparison line 42
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalEntryBudget_le_exp line 127
3. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_tolerance line 139
4. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_product_data line 213
5. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_product_comparison line 338
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_positive_spatial_comparison line 388