OAI/NumberTheory/TwoPoint/Circuits/CircuitPolynomialAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Algebra of the low-degree functions used in the circuit approximation. Multiplication adds degrees, including after Boolean multilinearization.

  1. lemma OAI.TwoPointCorrelations.walsh_mul line 16
  2. lemma OAI.TwoPointCorrelations.WalshDegreeLE.of_walsh line 35
  3. lemma OAI.TwoPointCorrelations.WalshDegreeLE.const line 41
  4. lemma OAI.TwoPointCorrelations.WalshDegreeLE.smul line 47
  5. lemma OAI.TwoPointCorrelations.WalshDegreeLE.sub line 58
  6. lemma OAI.TwoPointCorrelations.WalshDegreeLE.sum line 71
  7. lemma OAI.TwoPointCorrelations.WalshDegreeLE.mul line 85