OAI/NumberTheory/TwoPoint/Circuits/CircuitApproximationDegree.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Degree bookkeeping for the random polynomial construction. The recursive degree uses the largest child degree, rather than the number of leaves.

  1. lemma OAI.TwoPointCorrelations.WalshDegreeLE.mono line 13
  2. lemma OAI.TwoPointCorrelations.literal_indicator_degree line 26
  3. def OAI.TwoPointCorrelations.AC0Circuit.approximationDegree line 44