OAI/MeasureTheory/Falconer/Incidence/FrozenCoarseObstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The final contradiction for a regular coarse configuration whose original fine packets have been frozen to comparable sizes.

  1. theorem OAI.Falconer.frozen_coarse_packet_impossible line 13