OAI/Probability/InvariantIsing/Fields/SpinHammingEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The deterministic energy cost of changing a prescribed number of spins. These bounds apply to the slice comparisons in the magnetic theorem.

  1. lemma OAI.InvariantIsing.spinVector_sub_norm_sq line 13
  2. lemma OAI.InvariantIsing.sum_abs_spinValue_sub line 24
  3. lemma OAI.InvariantIsing.abs_fieldEnergy_sub_spin_le line 33
  4. lemma OAI.InvariantIsing.abs_rotatedEnergy_sub_spin_le line 52