OAI/MeasureTheory/Falconer/Shells/InverseShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The integrated inverse is controlled by independent endpoint energies

This applies the finite shell estimate to the exact original-pair inverse identity. The index set is the finite union of the actual inverse factors.

  1. theorem OAI.Falconer.integrated_inverse_shell_le line 15