OAI/MeasureTheory/Falconer/Incidence/RegularCoarsePencils.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A regular coarse pencil with a lower fine-incidence count in every retained coarse tube, obtained directly from the original fine pencils.

  1. theorem OAI.Falconer.regular_coarse_pencil_mul line 11
  2. theorem OAI.Falconer.regular_coarse_pencil line 59