OAI/NumberTheory/TwoPoint/Circuits/CircuitFiniteCodes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite alphabet for query positions and responses. Allowing one separator per block at most doubles the length of a query code.

  1. abbrev OAI.TwoPointCorrelations.BoundedRestrictionCode line 14
  2. def OAI.TwoPointCorrelations.readRestrictionCode line 17
  3. def OAI.TwoPointCorrelations.packRestrictionSymbol line 21
  4. lemma OAI.TwoPointCorrelations.read_packRestrictionSymbol line 27
  5. def OAI.TwoPointCorrelations.packRestrictionCode line 34
  6. lemma OAI.TwoPointCorrelations.read_packRestrictionCode line 40
  7. lemma OAI.TwoPointCorrelations.boundedRestrictionCode_card line 48
  8. lemma OAI.TwoPointCorrelations.two_mul_add_one_le_three_pow line 62
  9. lemma OAI.TwoPointCorrelations.boundedRestrictionCode_card_queries line 70