OAI/MeasureTheory/Falconer/Estimates/SourceClassOriginalLaws.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Source regularization preserves almost-everywhere bounds for the original reverse laws

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

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

  2. theorem OAI.Falconer.Regularization.sourceClass_conditional_absolutelyContinuous line 18
  3. theorem OAI.Falconer.Regularization.sourceClass_original_ae line 23
  4. theorem OAI.Falconer.Regularization.sourceClass_conditional_original_ae line 28