OAI/Probability/InvariantIsing/Magnetic/MagneticPartitionSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The constrained scalar-field supporting inequality on arbitrary finite partitions, expressed through the physical magnetic overlap path.

  1. lemma OAI.InvariantIsing.magneticFieldPath_step_ae line 16
  2. lemma OAI.InvariantIsing.fieldPairing_magnetic_same line 24
  3. lemma OAI.InvariantIsing.fieldPairing_magnetic_self line 39
  4. lemma OAI.InvariantIsing.magneticField_support_same_partition line 47
  5. lemma OAI.InvariantIsing.magneticField_support_equal_cutList line 71
  6. theorem OAI.InvariantIsing.magneticField_support line 78
  7. theorem OAI.InvariantIsing.magneticField_support_pairing line 92