OAI/NumberTheory/TwoPoint/Circuits/CircuitFourierDegree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A polynomial degree bound and exponential Fourier error, with no analytic parameter hypotheses left over from the switching argument.

  1. def OAI.TwoPointCorrelations.switchingDenominator line 12
  2. def OAI.TwoPointCorrelations.switchingDegree line 14
  3. lemma OAI.TwoPointCorrelations.switchingDenominator_pos line 16
  4. theorem OAI.TwoPointCorrelations.AC0Circuit.fourier_tail_polynomial_degree line 20