OAI/NumberTheory/TwoPoint/Circuits/CircuitWalkImage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The switching encoding changes each queried block to the values that satisfy its term. Query blocks are disjoint, so their responses can later be restored without disturbing the remaining encoding.

  1. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_eq_outside line 17
  2. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_extends line 27
  3. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_free line 37
  4. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_assign_comm line 47
  5. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_eq_assign line 57
  6. lemma OAI.TwoPointCorrelations.DNFQueryBlock.image_compatible line 71
  7. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.image_extends line 83
  8. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.step_image_compatible line 88
  9. lemma OAI.TwoPointCorrelations.CanonicalDNFWalk.step_image_restore line 102
  10. theorem OAI.TwoPointCorrelations.CanonicalDNFWalk.image_weight line 113