OAI/Combinatorics/Progressions/Estimates/EmptyLayerDetectionGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.euclideanFromCoordinates_lipschitz line 15
2. def OAI.Erdos3.mixedDensityCovolumeRatio line 31
3. theorem OAI.Erdos3.mixedDensityCovolumeRatio_pos line 35
4. def OAI.Erdos3.mixedAmbientInterpolation line 41
5. theorem OAI.Erdos3.mixedAmbientInterpolation_grid line 46
6. theorem OAI.Erdos3.mixedAmbientInterpolation_bounds line 61
7. theorem OAI.Erdos3.latticeSection_covolume_eq_one_of_isEmpty line 97
8. theorem OAI.Erdos3.mixedDensityCovolumeRatio_eq_one_of_isEmpty line 110