OAI/Computability/DepthThree/RestrictionCostCorrelation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.pathMixture_eq_pathTerm line 18
  2. theorem OAI.DepthThreeLowerBound.pathTerm_zero_of_incompatible line 31
  3. theorem OAI.DepthThreeLowerBound.abs_corr_pathTerm_le line 40
  4. def OAI.DepthThreeLowerBound.pathLayer line 83
  5. theorem OAI.DepthThreeLowerBound.abs_corr_pathLayer_le line 90
  6. theorem OAI.DepthThreeLowerBound.indexedCNF_restriction_expansion line 124
  7. theorem OAI.DepthThreeLowerBound.initial_and_live_path_cost_le line 141
  8. theorem OAI.DepthThreeLowerBound.restricted_correlation_le_cost line 155