OAI/MeasureTheory/Falconer/Graphs/CoordinateGraph.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A finite planar set is exactly the edge set of its two coordinate projections. This keeps original point counts in the dense graph reduction.

  1. theorem OAI.Falconer.rowPoint_coordinates line 10
  2. theorem OAI.Falconer.coordinate_graph_count line 14
  3. theorem OAI.Falconer.coordinate_graph_card_le line 35
  4. theorem OAI.Falconer.coordinate_graph_comparable line 42
  5. theorem OAI.Falconer.coordinate_graph_density line 56