OAI/MeasureTheory/Falconer/Recursion/ProfileEnvelopes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Profile lower bounds from the original mass law

An original s-ball estimate yields the lower profile bound after paying for class normalization and the dimension-dependent interpolation loss.

  1. theorem OAI.Falconer.Regularization.sourceClass_occupied_comparison line 17
  2. theorem OAI.Falconer.Regularization.normalizedClass_real_le line 36
  3. theorem OAI.Falconer.Regularization.sourceProfile_frostman_lower line 47