OAI/MeasureTheory/Falconer/Recursion/RetainedPairMasks.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.actualClassDomain line 9
  2. def OAI.PlanarFalconer.actualClassMeasure line 12
  3. theorem OAI.PlanarFalconer.actualClassDomain_disjoint line 15
  4. theorem OAI.PlanarFalconer.measurableSet_actualClassDomain line 25
  5. def OAI.PlanarFalconer.retainedPairs line 28
  6. def OAI.PlanarFalconer.retainedPairMask line 33
  7. def OAI.PlanarFalconer.restoredShellMask line 41
  8. theorem OAI.PlanarFalconer.measurable_retainedPairMask line 46
  9. theorem OAI.PlanarFalconer.measurable_restoredShellMask line 56
  10. theorem OAI.PlanarFalconer.restoredShellMask_le_one line 69
  11. theorem OAI.PlanarFalconer.restoredShellMask_on_pair line 79
  12. theorem OAI.PlanarFalconer.restoredShellMask_discarded line 108