OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionDistribution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The three-valued restriction law is exactly the experiment that first chooses live bits and then independent uniform values for the fixed bits.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_pair line 14
  2. lemma OAI.TwoPointCorrelations.bernoulli_half_average line 36
  3. def OAI.TwoPointCorrelations.partialAssignmentOfMask line 46
  4. lemma OAI.TwoPointCorrelations.partialAssignmentOfMask_apply line 49
  5. lemma OAI.TwoPointCorrelations.restriction_pair_atom line 55
  6. theorem OAI.TwoPointCorrelations.restrictionLaw_average line 66