OAI/MeasureTheory/Falconer/Incidence/PlanarIncidence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative planar measure incidence obstruction

This is the measure-to-finite-set step of ang:planar-measures. The only published input is the finite-set specialization of the planar Furstenberg theorem. All losses from the two original-label sampling steps are explicit; no geometric gain is assumed.

  1. def OAI.Falconer.samplingBallLoss line 18
  2. theorem OAI.Falconer.samplingBallLoss_pos line 20
  3. theorem OAI.Falconer.planar_measure_incidence_obstruction line 27