OAI/MeasureTheory/Falconer/Estimates/RegularClasses.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Regular classes of an original Frostman law in arbitrary dimension

This proves the application-level form of Lemma reg:regularization. The classes are unions of the original half-open leaves.

  1. structure OAI.Falconer.Regularization.RegularizedProfileData line 18
  2. theorem OAI.Falconer.Regularization.sourceClass_profile_data line 33
  3. theorem OAI.Falconer.Regularization.actual_regular_classes line 50