OAI/MeasureTheory/FalconerCompletion/Measures/PathIndex.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.CurrentFalconer.TreeND.pathIndex line 15
  2. lemma OAI.CurrentFalconer.TreeND.pathIndex_lt line 19
  3. lemma OAI.CurrentFalconer.TreeND.pathIndex_div_leading line 26
  4. lemma OAI.CurrentFalconer.TreeND.pathIndex_injective line 33
  5. lemma OAI.CurrentFalconer.TreeND.exists_pathIndex line 55
  6. lemma OAI.CurrentFalconer.TreeND.pathIndex_take line 79
  7. def OAI.CurrentFalconer.TreeND.treeCell line 97
  8. lemma OAI.CurrentFalconer.TreeND.measurableSet_treeCell line 100
  9. lemma OAI.CurrentFalconer.TreeND.treeCell_disjoint line 103
  10. lemma OAI.CurrentFalconer.TreeND.treeCell_subset_take line 115
  11. lemma OAI.CurrentFalconer.TreeND.treeCell_cover_root line 128