OAI/Probability/InvariantIsing/Fields/SpinGroupProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A nearest projection to all group constraints at once. Its number of changed spins is exactly the sum of the group count discrepancies.

  1. lemma OAI.InvariantIsing.exists_subset_card_nearest line 14
  2. lemma OAI.InvariantIsing.exists_spin_group_projection line 41
  3. def OAI.InvariantIsing.spinGroupProjection line 80
  4. lemma OAI.InvariantIsing.spinGroupProjection_mem line 84
  5. lemma OAI.InvariantIsing.spinGroupProjection_distance line 89