OAI/NumberTheory/TwoPoint/Circuits/CircuitRandomRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transfer from low-degree approximation after a random restriction to the Fourier tail of the original function. All probability spaces are finite.

  1. theorem OAI.TwoPointCorrelations.restriction_fourier_average line 15
  2. theorem OAI.TwoPointCorrelations.fourier_tail_le_random_restriction line 40
  3. lemma OAI.TwoPointCorrelations.walshTruncation_error_le_square line 62
  4. lemma OAI.TwoPointCorrelations.walshTruncation_error_eq_zero line 69