OAI/Probability/InvariantIsing/Magnetic/MagneticAdjacentCurvature.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Moving a nonnegative variance increment from a larger exponent to the preceding smaller exponent decreases the actual inverse curvature.

  1. lemma OAI.InvariantIsing.positive_cons line 14
  2. lemma OAI.InvariantIsing.upper_cons line 22
  3. theorem OAI.InvariantIsing.magneticClosedCurvature_adjacent_transfer line 30