OAI/NumberTheory/TwoPoint/Circuits/CircuitRandomGate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial gate replacement. A sampled subset contributes a linear factor that is one on an all-true input and zero when the subset contains exactly one false input. Repetition is a product of these factors.

  1. lemma OAI.TwoPointCorrelations.WalshDegreeLE.prod line 16
  2. def OAI.TwoPointCorrelations.andGateFactor line 34
  3. def OAI.TwoPointCorrelations.andGatePolynomial line 37
  4. lemma OAI.TwoPointCorrelations.WalshDegreeLE.andGateFactor line 41
  5. lemma OAI.TwoPointCorrelations.WalshDegreeLE.andGatePolynomial line 49
  6. lemma OAI.TwoPointCorrelations.andGateFactor_all_true line 61
  7. lemma OAI.TwoPointCorrelations.andGateFactor_one_false line 71
  8. lemma OAI.TwoPointCorrelations.andGatePolynomial_all_true line 86
  9. lemma OAI.TwoPointCorrelations.andGatePolynomial_isolated_false line 94