OAI/Computability/DepthThree/RestrictionExpectedCost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.pathCoveredCount_eq_of_support line 17
  2. theorem OAI.DepthThreeLowerBound.pathWeight_eq_coveredPathWeight_of_support line 40
  3. theorem OAI.DepthThreeLowerBound.pathWeight_eq_finiteAvg_supported line 52
  4. def OAI.DepthThreeLowerBound.fullAssignmentPathCost line 96
  5. theorem OAI.DepthThreeLowerBound.pathCost_eq_finiteAvg_supported line 105
  6. theorem OAI.DepthThreeLowerBound.restrictionAvg_pathCost_reweight line 115
  7. theorem OAI.DepthThreeLowerBound.restrictionAvg_pathCost_le line 132
  8. theorem OAI.DepthThreeLowerBound.restrictionAvg_restrictionCost_le_sum line 147
  9. theorem OAI.DepthThreeLowerBound.restrictionAvg_restrictionCost_le line 163