OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionFourier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality after fixing coordinates. Averaging over the fixed bits removes all cross terms with different original Walsh supports.

  1. lemma OAI.TwoPointCorrelations.restricted_walshCoefficient line 13
  2. lemma OAI.TwoPointCorrelations.restriction_support_injective line 37
  3. theorem OAI.TwoPointCorrelations.restricted_walshCoefficient_mean_sq line 44
  4. theorem OAI.TwoPointCorrelations.restricted_fourier_tail_mean line 78