OAI/Combinatorics/Progressions/Geometry/CanonicalSpatialSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.normalizedFiber_output_row line 14
2. theorem OAI.Erdos3.normalizedFiberDensity_zero_of_row line 27
3. theorem OAI.Erdos3.normalizedFiberDensity_row_bound line 73
4. theorem OAI.Erdos3.selectedColumn_sum line 97
5. theorem OAI.Erdos3.selectedSpatial_root_row_mass line 106
6. theorem OAI.Erdos3.selectedSpatial_slope_row_mass line 115
7. theorem OAI.Erdos3.canonicalSpatialSiteDensity_star_bound line 123
8. theorem OAI.Erdos3.canonicalSpatialSiteDensity_zero_outside line 170