OAI/MeasureTheory/Falconer/Recursion/TwoProfileInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact inverse factors with two independent original profiles

The finite output symbols are the same uniformly constructed symbols. Only their endpoint evaluations use the two distinct cubes, laws, profiles and mask families. Radius powers still charge only new derivatives.

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