OAI/Probability/InvariantIsing/Magnetic/MagneticGroupPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The weighted overlap path for the same field groups as the magnetic variational functional.

  1. def OAI.InvariantIsing.magneticGroupLevel line 13
  2. lemma OAI.InvariantIsing.magneticGroupLevel_mem_unit line 16
  3. lemma OAI.InvariantIsing.magneticGroupLevel_monotone line 26
  4. def OAI.InvariantIsing.magneticGroupPath line 33
  5. lemma OAI.InvariantIsing.magneticGroupPath_on_cell line 38
  6. lemma OAI.InvariantIsing.magneticGroupPath_eq_sum line 44