OAI/MeasureTheory/Falconer/Geometry/PlanarGridCosts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit fixed polynomial costs for the original-to-rounded graph construction. These are absorbed only after the geometric application.

  1. theorem OAI.Falconer.planar_grid_polynomial_costs line 9
  2. theorem OAI.Falconer.planar_direction_polynomial_cost line 58