OAI/MeasureTheory/Falconer/Shells/TwoRootMasks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.twoRootPairMask line 9
  2. theorem OAI.PlanarFalconer.measurable_twoRootPairMask line 15
  3. theorem OAI.PlanarFalconer.twoRootPairMask_le_one line 33
  4. def OAI.PlanarFalconer.retainedRootPairs line 41
  5. def OAI.PlanarFalconer.twoRootRetainedMask line 46
  6. def OAI.PlanarFalconer.restoredTwoRootMask line 53
  7. theorem OAI.PlanarFalconer.measurable_twoRootRetainedMask line 58
  8. theorem OAI.PlanarFalconer.measurable_restoredTwoRootMask line 64
  9. theorem OAI.PlanarFalconer.twoRoot_domain_unique line 69
  10. theorem OAI.PlanarFalconer.restoredTwoRootMask_on_pair line 79
  11. theorem OAI.PlanarFalconer.restoredTwoRootMask_discarded line 94
  12. theorem OAI.PlanarFalconer.restoredTwoRootMask_le_one line 108
  13. theorem OAI.PlanarFalconer.restoredTwoRootMask_empty line 124