OAI/Probability/InvariantIsing/Cavity/OffsetBlockSymmetry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Even permutations of the repeated blocks preserve an arbitrary initial remainder.

  1. def OAI.InvariantIsing.offsetBlockSitePermutation line 11
  2. lemma OAI.InvariantIsing.offsetBlockSitePermutation_prefix line 16
  3. lemma OAI.InvariantIsing.offsetBlockSitePermutation_block line 20
  4. lemma OAI.InvariantIsing.offsetBlockSitePermutation_sign line 24
  5. lemma OAI.InvariantIsing.offsetBlockConstraint_permutation line 29