OAI/MeasureTheory/Falconer/Recursion/BranchTransitions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PlanarFalconer.BranchState line 8
  2. def OAI.PlanarFalconer.BranchState.start line 15
  3. def OAI.PlanarFalconer.BranchState.finish line 17
  4. def OAI.PlanarFalconer.BranchState.index line 19
  5. def OAI.PlanarFalconer.BranchState.angular line 21
  6. def OAI.PlanarFalconer.BranchState.Valid line 25
  7. def OAI.PlanarFalconer.BranchState.descriptors line 29
  8. def OAI.PlanarFalconer.BranchState.nearDepth line 33
  9. theorem OAI.PlanarFalconer.BranchState.valid_depths line 36
  10. inductive OAI.PlanarFalconer.BranchLabel line 44
  11. inductive OAI.PlanarFalconer.BranchStep line 48
  12. theorem OAI.PlanarFalconer.BranchStep.nonterminal line 76
  13. theorem OAI.PlanarFalconer.BranchStep.nested line 79
  14. theorem OAI.PlanarFalconer.BranchStep.index_change line 99
  15. theorem OAI.PlanarFalconer.BranchStep.episode_balance line 103
  16. theorem OAI.PlanarFalconer.BranchStep.suffix_decrease line 108
  17. theorem OAI.PlanarFalconer.BranchStep.low_decrease line 116
  18. theorem OAI.PlanarFalconer.BranchStep.graph_charge line 121
  19. def OAI.PlanarFalconer.ChargedNear line 135
  20. theorem OAI.PlanarFalconer.near_uncharged_next_direct line 140