OAI/MeasureTheory/Falconer/Geometry/DyadicClasses.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.leafUnion line 10
  2. theorem OAI.PlanarFalconer.leafUnion_measurable line 13
  3. theorem OAI.PlanarFalconer.leafUnion_subset line 17
  4. theorem OAI.PlanarFalconer.leafUnion_mono line 23
  5. theorem OAI.PlanarFalconer.leafUnion_all line 29
  6. theorem OAI.PlanarFalconer.leafUnion_disjoint line 36
  7. theorem OAI.PlanarFalconer.measure_leafUnion line 50
  8. theorem OAI.PlanarFalconer.dyadicPaths_card_le line 60
  9. def OAI.PlanarFalconer.retainedLeaves line 74
  10. theorem OAI.PlanarFalconer.discarded_leaves_mass line 79
  11. def OAI.PlanarFalconer.classLeaves line 98
  12. def OAI.PlanarFalconer.classMeasure line 103
  13. theorem OAI.PlanarFalconer.classLeaves_disjoint line 107
  14. theorem OAI.PlanarFalconer.leafUnion_classes line 115
  15. theorem OAI.PlanarFalconer.class_mass_sum line 130
  16. theorem OAI.PlanarFalconer.discarded_classes_mass line 144
  17. def OAI.PlanarFalconer.normalizedClass line 163
  18. theorem OAI.PlanarFalconer.normalizedClass_probability line 167
  19. theorem OAI.PlanarFalconer.normalizedClass_apply line 178