OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The spectral consequence of simplifying a Boolean function under random restrictions: only restrictions whose decision trees remain deep contribute.

  1. lemma OAI.TwoPointCorrelations.restricted_error_le_degree_failure line 12
  2. theorem OAI.TwoPointCorrelations.fourier_tail_le_degree_failure line 28
  3. lemma OAI.TwoPointCorrelations.degree_failure_le_decision_tree_failure line 44