OAI/Combinatorics/Progressions/Geometry/NormalizedSpatialChoiceBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.normalizedSpatialShare line 9
2. def OAI.Erdos3.normalizedSpatialSiteAccuracy line 11
3. def OAI.Erdos3.normalizedSpatialPointAccuracy line 14
4. def OAI.Erdos3.normalizedSpatialResolution line 17
5. theorem OAI.Erdos3.normalizedSpatial_error_choices line 20
6. def OAI.Erdos3.normalizedSpatialPointLog line 121
7. theorem OAI.Erdos3.normalizedSpatialPointLog_nonneg line 124
8. theorem OAI.Erdos3.normalizedSpatialSiteAccuracy_inv_exp line 129
9. theorem OAI.Erdos3.normalizedSpatialPointAccuracy_inv_exp line 140
10. theorem OAI.Erdos3.normalizedSpatial_narrow_width_inv_exp line 168