OAI/MeasureTheory/Falconer/Recursion/ProfileLipschitz.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual regularized branching profile has the global Lipschitz bound required by quantitative differentiation, including its constant tails.

  1. theorem OAI.Falconer.Regularization.finiteRampProfile_increment_all line 10
  2. theorem OAI.Falconer.Regularization.planarProfile_lipschitz line 36
  3. theorem OAI.Falconer.Regularization.planarProfile_linear_decomposition line 65