OAI/Probability/InvariantIsing/Cavity/CavityRotationLogMean.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.cavityRotationLogMean line 16
  2. lemma OAI.InvariantIsing.measurable_cavityRotationLogMean line 24
  3. lemma OAI.InvariantIsing.cavityRotationLogMean_bound line 31
  4. lemma OAI.InvariantIsing.integrable_cavityRotationLogMean line 42