OAI/MeasureTheory/Falconer/Incidence/PlanarBaselineIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The elementary incidence bound at one dyadic scale. This is the baseline bound, before the strict gain from regular scales in the Furstenberg proof.

  1. theorem OAI.Falconer.planar_baseline_incidence line 14