OAI/Probability/InvariantIsing/Magnetic/MagneticSliceFieldBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact magnetization-slice field bound for the zero-temperature boundary of the magnetic contact comparison.

  1. lemma OAI.InvariantIsing.constrainedBlockValue_group_le line 13
  2. lemma OAI.InvariantIsing.constrainedBlockValue_entropy_bound line 34