OAI/MeasureTheory/Falconer/Measures/ClassSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Original support and occupied anchors of the normalized classes

  1. theorem OAI.Falconer.ae_occupied_anchors line 12
  2. theorem OAI.Falconer.Regularization.normalizedClass_absolutelyContinuous line 26
  3. theorem OAI.Falconer.Regularization.sourceClass_absolutelyContinuous line 31

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Estimates/SourceClassOriginalLaws.lean:12 (same statement text; different proof or body). Qualify references as OAI.Falconer.Regularization.sourceClass_absolutelyContinuous@path.

  4. theorem OAI.Falconer.Regularization.normalizedClass_parent line 35
  5. theorem OAI.Falconer.Regularization.sourceClass_parent line 45