OAI/Computability/DepthThree/RestrictionPathData.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.pathCompatible line 18
  2. def OAI.DepthThreeLowerBound.pathCenter line 21
  3. theorem OAI.DepthThreeLowerBound.pathCenter_support line 24
  4. theorem OAI.DepthThreeLowerBound.pathCompatible_nil line 36
  5. def OAI.DepthThreeLowerBound.pathPrefixSet line 45
  6. def OAI.DepthThreeLowerBound.pathFinalSet line 49
  7. def OAI.DepthThreeLowerBound.pathLiveSet line 52
  8. def OAI.DepthThreeLowerBound.pathCoveredCount line 56
  9. def OAI.DepthThreeLowerBound.pathWeight line 61
  10. def OAI.DepthThreeLowerBound.pathCost line 64
  11. def OAI.DepthThreeLowerBound.restrictionCost line 68
  12. theorem OAI.DepthThreeLowerBound.pathWeight_nonneg line 71
  13. theorem OAI.DepthThreeLowerBound.pathCost_nonneg line 75
  14. theorem OAI.DepthThreeLowerBound.restrictionCost_nonneg line 83
  15. theorem OAI.DepthThreeLowerBound.pathWeight_nil line 87
  16. theorem OAI.DepthThreeLowerBound.pathCost_zero line 90
  17. theorem OAI.DepthThreeLowerBound.pathPrefixSet_subset_final line 94
  18. theorem OAI.DepthThreeLowerBound.pathCoveredCount_pos line 104
  19. theorem OAI.DepthThreeLowerBound.pathLiveSet_image line 124
  20. theorem OAI.DepthThreeLowerBound.pathLiveSet_card line 141
  21. theorem OAI.DepthThreeLowerBound.path_support_iff_live_cylinder line 146
  22. theorem OAI.DepthThreeLowerBound.path_cylinder_probability line 165