OAI/MeasureTheory/Falconer/Estimates/PlanarGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Planar measure projection gain from the published Furstenberg input

This gives a fixed positive power bound for incidence with small parallel strip covers. Both coordinate maps may identify original labels. The conclusion is proved from the cited finite Furstenberg theorem through the two-stage sampling argument.

  1. theorem OAI.Falconer.planar_measure_projection_gain line 19