OAI/MeasureTheory/Falconer/Geometry/RetainedCoarseCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The common-grid cover of retained fine lines is bounded by the retained incident coarse pencils, in the reverse direction needed when applying the regular-set alternative after refinement.

  1. theorem OAI.Falconer.rounded_candidates_reverse line 11
  2. theorem OAI.Falconer.retained_coarse_cover_card line 23