OAI/NumberTheory/TwoPoint/Circuits/CircuitRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Restrictions retain the coordinates in L and fix every other bit. Walsh characters factor into their live and fixed coordinates.

  1. def OAI.TwoPointCorrelations.restrictCube line 13
  2. lemma OAI.TwoPointCorrelations.walsh_restrictCube line 16
  3. lemma OAI.TwoPointCorrelations.WalshDegreeLE.restrict line 32