OAI/MeasureTheory/Falconer/Graphs/RoundedProjectionGraph.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact edge counts and original projection bounds for the rounded coordinate graphs, before any asymptotic loss absorption.

  1. theorem OAI.Falconer.roundedProjectionCoordinates_graph_count line 10
  2. theorem OAI.Falconer.roundedProjectionCoordinates_projection_cells line 27
  3. theorem OAI.Falconer.coordinate_graph_factor_lower line 53