OAI/NumberTheory/TwoPoint/Circuits/CircuitDecisionTree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A decision tree making at most d queries on any branch has Walsh degree at most d. This is the spectral consequence of circuit switching.

  1. lemma OAI.TwoPointCorrelations.WalshDegreeLE.add line 12
  2. inductive OAI.TwoPointCorrelations.BooleanDecisionTree line 20
  3. def OAI.TwoPointCorrelations.BooleanDecisionTree.eval line 26
  4. def OAI.TwoPointCorrelations.BooleanDecisionTree.depth line 30
  5. def OAI.TwoPointCorrelations.BooleanDecisionTree.indicator line 34
  6. theorem OAI.TwoPointCorrelations.BooleanDecisionTree.indicator_degree line 37
  7. lemma OAI.TwoPointCorrelations.WalshDegreeLE.high_coefficient_zero line 60