OAI/NumberTheory/TwoPoint/Circuits/CircuitBooleanOps.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Relabel, complement and conjoin the residue circuits used in a closed-word expansion without increasing their internal depth.

  1. def OAI.TwoPointCorrelations.AC0Circuit.negate line 12
  2. lemma OAI.TwoPointCorrelations.AC0Circuit.negate_eval line 17
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.negate_depth line 24
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.negate_size line 30
  5. def OAI.TwoPointCorrelations.AC0Circuit.relabel line 36
  6. lemma OAI.TwoPointCorrelations.AC0Circuit.relabel_eval line 39
  7. lemma OAI.TwoPointCorrelations.AC0Circuit.relabel_depth line 43
  8. lemma OAI.TwoPointCorrelations.AC0Circuit.relabel_size line 48
  9. def OAI.TwoPointCorrelations.AC0Circuit.conjunction line 53
  10. lemma OAI.TwoPointCorrelations.AC0Circuit.conjunction_eval line 57
  11. lemma OAI.TwoPointCorrelations.AC0Circuit.conjunction_depth line 67
  12. lemma OAI.TwoPointCorrelations.AC0Circuit.conjunction_size line 76