OAI/MeasureTheory/Falconer/Campaign123Development.lean

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

The Falconer distance conjecture in all dimensions

The all-dimensional theorem follows from planar Furstenberg incidence, higher-dimensional angular estimates, graph bounds and reconstruction of the original distance measure. The conditional implication from the planar Furstenberg estimate is also formalized.

This file declares nothing itself. It gathers the 1026 imports below, so a file that imports it gets all of them.

Imports