OAI/Probability/InvariantIsing/Fields/SpinSliceProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Attainability of every positive-spin count and deterministic projection to a nearest magnetization slice.

  1. def OAI.InvariantIsing.spinPositiveSites line 13
  2. def OAI.InvariantIsing.spinOfPositiveSites line 16
  3. lemma OAI.InvariantIsing.spinPositiveSites_of_set line 19
  4. lemma OAI.InvariantIsing.spinOfPositiveSites_of_spin line 24
  5. lemma OAI.InvariantIsing.spin_hamming_eq_symmDiff line 29
  6. lemma OAI.InvariantIsing.exists_spin_with_count_nearest line 37
  7. def OAI.InvariantIsing.spinCountProjection line 71
  8. lemma OAI.InvariantIsing.spinCountProjection_count line 74
  9. lemma OAI.InvariantIsing.spinCountProjection_distance line 78
  10. def OAI.InvariantIsing.spinCountSlice line 83
  11. lemma OAI.InvariantIsing.spinCountSlice_nonempty line 86
  12. lemma OAI.InvariantIsing.spinCountProjection_mem line 92