OAI/NumberTheory/TwoPoint/Circuits/CircuitDecisionDNF.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A decision tree of depth r is a DNF of width at most r. Both Boolean polarities have such a representation, so gates can be switched without counting the number of clauses produced by earlier switches.

  1. def OAI.TwoPointCorrelations.BooleanDecisionTree.negate line 16
  2. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.negate_eval line 20
  3. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.negate_depth line 27
  4. def OAI.TwoPointCorrelations.CubeTerm.withLiteral line 34
  5. lemma OAI.TwoPointCorrelations.CubeTerm.withLiteral_eval line 37
  6. def OAI.TwoPointCorrelations.addDNFLiteral line 60
  7. lemma OAI.TwoPointCorrelations.dnfEval_eq_true line 64
  8. lemma OAI.TwoPointCorrelations.addDNFLiteral_eval line 68
  9. lemma OAI.TwoPointCorrelations.addDNFLiteral_width line 90
  10. def OAI.TwoPointCorrelations.BooleanDecisionTree.toDNF line 103
  11. theorem OAI.TwoPointCorrelations.BooleanDecisionTree.toDNF_eval line 108
  12. theorem OAI.TwoPointCorrelations.BooleanDecisionTree.toDNF_width line 120