OAI/MeasureTheory/Falconer/Radial/HeavyDischarge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Discharging the application-level heavy-hyperplane input

The maximal heavy family has at most 2/m representatives. A substantial intersection forces the normals to be close, because transverse slabs have small mass by the stated single-scale codimension-two concentration bound.

  1. theorem OAI.Falconer.published_heavy_hyperplanes line 17