OAI/MeasureTheory/Falconer/Incidence/ComparableFrozenPencils.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Select comparable original coarse pencils and then freeze their fine packet sizes. Both selections retain explicit coarse-point mass.

  1. theorem OAI.Falconer.comparable_frozen_pencils line 12