OAI/MeasureTheory/Falconer/Geometry/ScalarRoundingCovers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar projection covers and ball counts are stable under the actual half-cell rounding used by the dyadic projection theorem.

  1. theorem OAI.Falconer.scalar_matched_projection_cover line 10
  2. theorem OAI.Falconer.scalar_image_ball_bound line 28