OAI/MeasureTheory/Falconer/Shells/InverseClassShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite inverse factors bounded by the next actual state

The finite coefficients are separated from the original endpoint transforms. Every energy on the right belongs to the exact descriptor class constructed by the inverse, with its remaining derivative budget.

  1. theorem OAI.Falconer.DescriptorInverseSymbols.finite_shell_le line 22