OAI/Probability/InvariantIsing/Cavity/ConsecutiveBlockPrior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Repeated identical cavity constraints admit every even permutation of their blocks. No coordinate sign flip is introduced.

  1. def OAI.InvariantIsing.consecutiveBlockConstraint line 14
  2. lemma OAI.InvariantIsing.mem_consecutiveBlockConstraint line 17
  3. lemma OAI.InvariantIsing.consecutiveBlockConstraint_nonempty line 22
  4. def OAI.InvariantIsing.consecutiveBlockSitePermutation line 30
  5. lemma OAI.InvariantIsing.consecutiveBlockSitePermutation_apply line 33
  6. lemma OAI.InvariantIsing.consecutiveBlockSitePermutation_sign line 38
  7. lemma OAI.InvariantIsing.consecutiveBlockSitePermutation_flip line 43
  8. lemma OAI.InvariantIsing.consecutiveBlockConstraint_permutation line 49
  9. theorem OAI.InvariantIsing.consecutiveBlockPrior_permutation line 71