OAI/Probability/InvariantIsing/Fields/SpinGroupSlice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite magnetization slices for an arbitrary grouping of the sites. Constant group fields factor exactly, with the original cube mass.

  1. def OAI.InvariantIsing.spinGroupSize line 13
  2. def OAI.InvariantIsing.spinGroupCount line 17
  3. def OAI.InvariantIsing.spinGroupSlice line 21
  4. lemma OAI.InvariantIsing.spinGroupSlice_nonempty line 25
  5. lemma OAI.InvariantIsing.sum_spinValue_eq_count line 46
  6. lemma OAI.InvariantIsing.fieldEnergy_group_counts line 55
  7. def OAI.InvariantIsing.spinGroupFieldConstant line 73
  8. lemma OAI.InvariantIsing.fieldEnergy_on_group_slice line 77
  9. lemma OAI.InvariantIsing.restrictedSpinLog_group_field line 85