OAI/MeasureTheory/Falconer/Estimates/DyadicEnergyStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From integrated localization to the original independent energy

This is the algebraic assembly step: exact original-law splitting, the actual cap partition, integrated localization, and the proved Schur bound. The localization premise is supplied by dyadic_localization_error.

  1. theorem OAI.Falconer.independentAngularEnergy_of_localization line 19