OAI/MeasureTheory/Falconer/Graphs/RoundedGraphData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original planar point and projection counts determine all size parameters in the rounded graph.

  1. theorem OAI.Falconer.rounded_graph_size_bounds line 9
  2. theorem OAI.Falconer.rounded_graph_density_bound line 47