OAI/Probability/InvariantIsing/Magnetic/RestrictedCanonicalHaarLog.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The constrained base Gibbs law and independent fresh group frames in the actual canonical capped logarithm.

  1. def OAI.InvariantIsing.restrictedCanonicalHaarLog line 16
  2. lemma OAI.InvariantIsing.measurable_restrictedCanonicalHaarLog line 32
  3. lemma OAI.InvariantIsing.restrictedCanonicalHaarLog_bound line 42