OAI/Probability/InvariantIsing/Fields/SpinSliceComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Deterministic comparison of restricted pressures through bounded spin-flip maps, including the multiplicity cost of those maps.

  1. lemma OAI.InvariantIsing.rotated_spin_energy_map_bound line 13
  2. lemma OAI.InvariantIsing.restricted_spin_pressure_map_le line 35
  3. lemma OAI.InvariantIsing.abs_restricted_spin_pressure_sub_le line 50