OAI/MeasureTheory/Falconer/Recursion/UniformProfileGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform gain for the actual regularized planar profile, assuming only its finite branching-count lower growth. All decomposition and recursion parameters are chosen before the configuration and the depth.

  1. theorem OAI.Falconer.uniform_profile_endpoint_gain line 13