OAI/MeasureTheory/Falconer/Incidence/NormalizedProductPencils.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Assemble the common-row rounding into actual pencil families. The pencil cardinality drops by at most 361, and the complete union grows by at most 361. No separation assumption is needed on the original union.

  1. def OAI.Falconer.normalizedPencil line 11
  2. def OAI.Falconer.normalizedRowPencils line 14
  3. theorem OAI.Falconer.normalizedPencil_card_upper line 18
  4. theorem OAI.Falconer.normalizedPencil_card_lower line 22
  5. theorem OAI.Falconer.normalizedPencil_nonempty line 31
  6. theorem OAI.Falconer.normalizedPencil_incident line 35
  7. theorem OAI.Falconer.normalizedPencil_chart line 43
  8. theorem OAI.Falconer.normalizedPencil_regular line 52
  9. theorem OAI.Falconer.normalizedRowPencils_union line 67
  10. theorem OAI.Falconer.normalizedRowPencils_union_separated line 74
  11. theorem OAI.Falconer.normalizedRowPencils_union_card line 80