OAI/NumberTheory/TwoPoint/Circuits/CircuitFourierSwitching.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Fourier concentration obtained from the proved switching estimate. All parameters remain explicit for the fixed-depth application.

  1. theorem OAI.TwoPointCorrelations.fourier_tail_le_small_tree_failure line 13
  2. theorem OAI.TwoPointCorrelations.AC0Circuit.fourier_tail_switching line 45