OAI/Probability/InvariantIsing/Magnetic/MagneticPopulationCoupling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transporting a magnetization profile through a finite coupling of field populations increases its grouped constrained entropy.

  1. def OAI.InvariantIsing.transportedMagnetization line 13
  2. lemma OAI.InvariantIsing.transportedMagnetization_radius line 17
  3. lemma OAI.InvariantIsing.transportedMagnetization_groupValue line 30
  4. lemma OAI.InvariantIsing.transportedMagnetization_variational line 65