OAI/Probability/InvariantIsing/Magnetic/MagneticGroupAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact passage from attainable block proportions to the weighted magnetic functional and overlap path.

  1. lemma OAI.InvariantIsing.sum_grouped_sites line 12
  2. lemma OAI.InvariantIsing.average_grouped_sites line 25
  3. lemma OAI.InvariantIsing.magneticGroupValue_eq_block line 36
  4. lemma OAI.InvariantIsing.magneticGroupLevel_eq_block line 44
  5. lemma OAI.InvariantIsing.magneticGroupPath_eq_block line 52