OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The three-valued product law for independent random restrictions. Fixing s previously free coordinates changes weight by an exact factor.

  1. def OAI.TwoPointCorrelations.restrictionBitLaw line 14
  2. def OAI.TwoPointCorrelations.restrictionLaw line 20
  3. theorem OAI.TwoPointCorrelations.restrictionLaw_assign_weight line 24
  4. theorem OAI.TwoPointCorrelations.FiniteLaw.probability_le_of_encoding line 45