OAI/MeasureTheory/Falconer/Incidence/RegularizedTubePencils.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The equal-cardinality reduction with all original incidence and non-concentration properties retained explicitly.

  1. theorem OAI.Falconer.regularize_tube_pencils line 11