OAI/Probability/InvariantIsing/Magnetic/RestrictedSpinLog.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Restricted spin sums retain the original cube mass. A deterministic map of slices costs its energy error and the logarithm of its largest fiber.

  1. def OAI.InvariantIsing.restrictedSpinLog line 13
  2. lemma OAI.InvariantIsing.restrictedSpinLog_univ line 16
  3. lemma OAI.InvariantIsing.restrictedSpinLog_add_const line 20
  4. lemma OAI.InvariantIsing.restrictedSpinLog_mono line 29
  5. lemma OAI.InvariantIsing.restrictedSpinLog_le_full line 37
  6. lemma OAI.InvariantIsing.sum_exp_le_of_fiber_bound line 42
  7. lemma OAI.InvariantIsing.restrictedSpinLog_le_of_map line 64