OAI/MeasureTheory/Falconer/Graphs/RoundedGraphCounts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Original cardinality bounds supply both coordinate comparability and graph density; no balance or density condition is added to the point set.

  1. theorem OAI.Falconer.coordinate_graph_scaled_bounds line 9
  2. theorem OAI.Falconer.roundedProjectionCoordinates_coordinate_upper line 32
  3. theorem OAI.Falconer.scalar_dilation_separated line 45