OAI/Probability/InvariantIsing/Fields/SpinFiniteCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite unions of spin constraints approximate the full partition function with an explicit spin-projection error and a finite-union cost.

  1. lemma OAI.InvariantIsing.sum_biUnion_le_sum_of_nonneg line 12
  2. lemma OAI.InvariantIsing.restrictedSpinLog_finite_union_le line 25
  3. lemma OAI.InvariantIsing.full_pressure_le_finite_cover line 55