OAI/Probability/InvariantIsing/Magnetic/MagneticRationalCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every bounded magnetization profile is close to one of finitely many rational interior profiles, including profiles at the boundary.

  1. lemma OAI.InvariantIsing.exists_interior_rat_close line 13
  2. lemma OAI.InvariantIsing.finite_rational_magnetization_cover line 28