OAI/MeasureTheory/Falconer/Recursion/ProfileNodeValues.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Values at the actual block depths, and the complementary descendant-count values used by the Frostman profile lower bound.

  1. theorem OAI.Falconer.Regularization.finiteRampProfile_prefix line 9
  2. def OAI.Falconer.Regularization.terminalBranchingProfile line 42
  3. theorem OAI.Falconer.Regularization.terminalBranchingProfile_zero line 46
  4. theorem OAI.Falconer.Regularization.terminalBranchingProfile_lipschitz line 50