OAI/MeasureTheory/Falconer/Incidence/CoarseSquashedPencils.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Prepare original bounded-chart pencils at the chosen terminal grid scale. All losses are fixed packing factors in the scale ratio.

  1. theorem OAI.Falconer.planarSquash_in_centeredUnitCube line 12
  2. theorem OAI.Falconer.coarse_squashed_pencil_configuration line 24