OAI/MeasureTheory/Falconer/Estimates/RegularizationClasses.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Regularization classes on the original all-dimensional dyadic tree

Classes are literal disjoint unions of half-open leaves. The measure identities and the discarded mass bounds hold for the original law.

  1. def OAI.Falconer.Regularization.leafUnion line 18
  2. theorem OAI.Falconer.Regularization.leafUnion_measurable line 21
  3. theorem OAI.Falconer.Regularization.leafUnion_subset line 25
  4. theorem OAI.Falconer.Regularization.leafUnion_mono line 31
  5. theorem OAI.Falconer.Regularization.leafUnion_all line 37
  6. theorem OAI.Falconer.Regularization.leafUnion_disjoint line 44
  7. theorem OAI.Falconer.Regularization.measure_leafUnion line 58
  8. def OAI.Falconer.Regularization.retainedLeaves line 68
  9. theorem OAI.Falconer.Regularization.discarded_leaves_mass line 73
  10. def OAI.Falconer.Regularization.classLeaves line 92
  11. def OAI.Falconer.Regularization.classMeasure line 97
  12. theorem OAI.Falconer.Regularization.classLeaves_disjoint line 101
  13. theorem OAI.Falconer.Regularization.leafUnion_classes line 109
  14. theorem OAI.Falconer.Regularization.class_mass_sum line 124
  15. theorem OAI.Falconer.Regularization.discarded_classes_mass line 138
  16. def OAI.Falconer.Regularization.normalizedClass line 157
  17. theorem OAI.Falconer.Regularization.normalizedClass_probability line 161
  18. theorem OAI.Falconer.Regularization.normalizedClass_apply line 172