OAI/MeasureTheory/Falconer/Recursion/UniformFrostmanProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One regularization choice for all measures with the fixed Frostman bound

  1. theorem OAI.Falconer.Regularization.uniform_frostman_profile_envelope line 12