OAI/MeasureTheory/Falconer/Recursion/BranchAnalyticSuccessors.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.AngularStateData.branchState line 13
  2. theorem OAI.PlanarFalconer.AngularStateData.branchState_descriptors line 15
  3. theorem OAI.PlanarFalconer.AngularStateData.successor_branchState line 18
  4. theorem OAI.PlanarFalconer.AngularStateData.near_branch_transition line 21
  5. theorem OAI.PlanarFalconer.AngularStateData.direct_branch_transition line 28
  6. def OAI.PlanarFalconer.PositiveDistanceData.branchState line 38
  7. def OAI.PlanarFalconer.PositiveDistanceData.branchProfile line 39
  8. def OAI.PlanarFalconer.PositiveDistanceData.angularSuccessor line 41
  9. theorem OAI.PlanarFalconer.PositiveDistanceData.angularSuccessor_energy line 44
  10. theorem OAI.PlanarFalconer.PositiveDistanceData.angularSuccessor_list_index line 49
  11. theorem OAI.PlanarFalconer.PositiveDistanceData.suffix_branch_transition line 54
  12. theorem OAI.PlanarFalconer.PositiveDistanceData.low_branch_transition line 60
  13. theorem OAI.PlanarFalconer.PositiveDistanceData.high_branch_transition line 67
  14. theorem OAI.PlanarFalconer.PositiveDistanceData.high_energy_member_transition line 75
  15. theorem OAI.PlanarFalconer.AngularStateData.far_branch_transition line 95
  16. theorem OAI.PlanarFalconer.AngularStateData.far_successor_list_index line 106