OAI/Probability/InvariantIsing/Magnetic/RestrictedCanonicalLogIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the canonical base partition and the random-block cavity logarithm under the product Haar law.

  1. lemma OAI.InvariantIsing.restricted_canonical_log_partition line 16
  2. lemma OAI.InvariantIsing.integrable_restricted_canonical_log_partition line 30
  3. lemma OAI.InvariantIsing.restricted_canonical_capped_log_bound line 42
  4. lemma OAI.InvariantIsing.integrable_restricted_canonical_capped_log line 59