OAI/Probability/InvariantIsing/Cavity/OffsetBlockPrior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed initial remainder followed by repeated constrained blocks. Adding a new last block preserves this exact finite spin family.

  1. def OAI.InvariantIsing.offsetBlockConstraint line 11
  2. lemma OAI.InvariantIsing.offsetBlockConstraint_nonempty line 15
  3. lemma OAI.InvariantIsing.mem_offsetBlockConstraint line 20
  4. def OAI.InvariantIsing.offsetBlockJoin line 28
  5. lemma OAI.InvariantIsing.offsetBlockJoin_mem line 31
  6. lemma OAI.InvariantIsing.offsetBlockConstraint_succ line 69
  7. lemma OAI.InvariantIsing.offsetBlockConstraint_card line 80
  8. lemma OAI.InvariantIsing.offsetBlockConstraint_log_mass line 84
  9. lemma OAI.InvariantIsing.offset_spin_family_succ line 93