OAI/MeasureTheory/Falconer/Incidence/SquashedPencils.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Original bounded-chart pencils, thinned by a fixed factor and moved to the slope chart required by the regular incidence estimate.

  1. def OAI.Falconer.squashedPencils line 11
  2. theorem OAI.Falconer.squashedPencils_at line 14
  3. theorem OAI.Falconer.squashedPencils_union line 18
  4. theorem OAI.Falconer.squashedPencils_union_card line 35
  5. theorem OAI.Falconer.squashed_pencil_configuration line 39