OAI/Probability/InvariantIsing/Fields/FieldHeightLists.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact transition-list laws for a literal height update.

  1. lemma OAI.InvariantIsing.fieldAllIncrements_withHeights line 13
  2. lemma OAI.InvariantIsing.fieldAllIncrements_update_interior line 25
  3. lemma OAI.InvariantIsing.fieldAllIncrements_update_final line 37
  4. lemma OAI.InvariantIsing.fieldAdjacentIncrements_root line 47