OAI/Computability/DepthThree/RestrictionMarkerCNF.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.residualCNF_eval_eq_true line 19
  2. theorem OAI.DepthThreeLowerBound.residualCNF_widthAtMost line 26
  3. def OAI.DepthThreeLowerBound.markerCNF line 34
  4. theorem OAI.DepthThreeLowerBound.markerCNF_eval line 38
  5. theorem OAI.DepthThreeLowerBound.markerCNF_widthAtMost line 47
  6. theorem OAI.DepthThreeLowerBound.markerCNF_avg line 61
  7. def OAI.DepthThreeLowerBound.markerProductCNF line 74
  8. theorem OAI.DepthThreeLowerBound.markerProductCNF_eval_eq_true line 78
  9. theorem OAI.DepthThreeLowerBound.markerProductCNF_indicator line 93
  10. theorem OAI.DepthThreeLowerBound.markerProductCNF_widthAtMost line 102
  11. theorem OAI.DepthThreeLowerBound.markerProductCNF_avg line 118
  12. def OAI.DepthThreeLowerBound.markerCylinderCNF line 129
  13. theorem OAI.DepthThreeLowerBound.markerCylinderCNF_widthAtMost line 134
  14. theorem OAI.DepthThreeLowerBound.markerCylinderCNF_avg line 146
  15. theorem OAI.DepthThreeLowerBound.markerCylinderCNF_scaled_avg line 165