OAI/Combinatorics/Progressions/Geometry/AllocatedOneCubeCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates line 25
2. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_jet line 32
3. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_physical_jets line 40
4. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_density line 52
5. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_bound_of_ne_zero line 91
6. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSiteCoordinates_zero_outside line 128
7. def OAI.Erdos3.VectorPolynomial.allocatedOneCubeFullLongJets line 159
8. theorem OAI.Erdos3.VectorPolynomial.allocatedOneCubeNormalizedSites_eq line 163