OAI/Probability/InvariantIsing/Magnetic/MagneticBlockPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The canonical site-average overlap path and its uniform comparison with the original constrained-block overlap path.

  1. def OAI.InvariantIsing.magneticBlockLevel line 14
  2. lemma OAI.InvariantIsing.magneticBlockLevel_mem_unit line 17
  3. lemma OAI.InvariantIsing.magneticBlockLevel_monotone line 30
  4. def OAI.InvariantIsing.magneticBlockPath line 36
  5. lemma OAI.InvariantIsing.magneticBlockPairMean_comparison line 40
  6. lemma OAI.InvariantIsing.magneticBlockPath_l1_comparison line 55