OAI/Computability/DepthThree/CircuitDeletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.Clause.violation_probability line 19
  2. theorem OAI.DepthThreeLowerBound.Clause.false_probability line 34
  3. def OAI.DepthThreeLowerBound.CNF.deleteWide line 44
  4. theorem OAI.DepthThreeLowerBound.CNF.mem_deleteWide line 47
  5. theorem OAI.DepthThreeLowerBound.CNF.deleteWide_nil line 51
  6. theorem OAI.DepthThreeLowerBound.CNF.deleteWide_cons line 55
  7. theorem OAI.DepthThreeLowerBound.CNF.deleteWide_widthAtMost line 60
  8. theorem OAI.DepthThreeLowerBound.CNF.deleteWide_normalized line 65
  9. theorem OAI.DepthThreeLowerBound.CNF.deleteWide_length_le line 70
  10. theorem OAI.DepthThreeLowerBound.CNF.eval_deleteWide_of_eval line 80
  11. theorem OAI.DepthThreeLowerBound.CNF.indicator_eval_le_deleteWide line 86
  12. theorem OAI.DepthThreeLowerBound.CNF.deletion_error_cons_le line 93
  13. theorem OAI.DepthThreeLowerBound.CNF.deletion_error_bound line 108