OAI/MeasureTheory/Falconer/Recursion/ReachedStateRecursion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.PolicyBranch.extend line 11
  2. theorem OAI.PlanarFalconer.PolicyBranch.extend_state_le line 28
  3. theorem OAI.PlanarFalconer.PolicyBranch.extend_label_lt line 33
  4. theorem OAI.PlanarFalconer.PolicyBranch.extend_last_state line 38
  5. theorem OAI.PlanarFalconer.PolicyBranch.extend_last_label line 43
  6. theorem OAI.PlanarFalconer.uniform_reached_branch_extension line 50
  7. def OAI.PlanarFalconer.SourceReached line 77
  8. theorem OAI.PlanarFalconer.SourceReached.valid line 82
  9. theorem OAI.PlanarFalconer.SourceReached.root line 88
  10. theorem OAI.PlanarFalconer.uniform_source_reached_successor line 92
  11. theorem OAI.PlanarFalconer.uniform_source_reached_induction line 112