OAI/Probability/InvariantIsing/Magnetic/RestrictedRotationLogMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-volume expected logarithmic partition function is measurable and integrable in the orthogonal disorder.

  1. def OAI.InvariantIsing.restrictedRotationLogMean line 17
  2. lemma OAI.InvariantIsing.measurable_restrictedRotationLogMean line 26
  3. lemma OAI.InvariantIsing.restrictedRotationLogMean_bound line 34
  4. lemma OAI.InvariantIsing.integrable_restrictedRotationLogMean line 46