OAI/MeasureTheory/Falconer/Graphs/GraphBallCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual graph edges in a narrow Cartesian strip are covered by planar balls. The count retains every neighbor, rather than only one witness.

  1. theorem OAI.Falconer.rowPoint_dist_le_sum line 10
  2. theorem OAI.Falconer.normalized_ball_bound_all_radii line 20
  3. theorem OAI.Falconer.scalar_graph_ball_cover line 33