OAI/Combinatorics/Progressions/Geometry/FixedSpatialEmptyCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.fixedSpatialEmptyIndex line 15
2. def OAI.Erdos3.fixedSpatialEmptyCoordinates line 27
3. theorem OAI.Erdos3.fixedSpatialEmptyCoordinates_apply line 49
4. theorem OAI.Erdos3.fixedSpatialEmptyCoordinates_symm_apply line 52
5. theorem OAI.Erdos3.fixedSpatialEmptyCoordinates_measurePreserving line 56
6. theorem OAI.Erdos3.fixedSpatialEmptyCoordinates_symm_measurePreserving line 67
7. def OAI.Erdos3.fixedSpatialEmptyDensity line 72
8. theorem OAI.Erdos3.fixedSpatialEmptyDensity_image_law line 76
9. theorem OAI.Erdos3.fixedSpatialEmptyDensity_probability_data line 87
10. theorem OAI.Erdos3.fixedSpatialEmptyDensity_bounds line 97
11. theorem OAI.Erdos3.fixedSpatialEmptyDensity_zero_outside line 113