OAI/Probability/InvariantIsing/Magnetic/RestrictedBlockConsistency.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Plateau consistency and the L1 self-consistency implication for the actual constrained block overlap, with arbitrary finite cascade depth.

  1. lemma OAI.InvariantIsing.restricted_finite_level_fiber line 15
  2. lemma OAI.InvariantIsing.restrictedBlockPairMean_eq_of_height_eq line 49
  3. lemma OAI.InvariantIsing.restrictedBlockOverlapPath_on_cell line 56
  4. lemma OAI.InvariantIsing.restrictedBlockOverlapPath_eq_of_cell_height_eq line 62
  5. theorem OAI.InvariantIsing.restricted_block_self_consistency_l1 line 73