OAI/Probability/InvariantIsing/Cavity/CavityCanonicalLogIntegrability.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.cavity_canonical_log_partition line 16
  2. lemma OAI.InvariantIsing.integrable_cavity_canonical_log_partition line 29
  3. lemma OAI.InvariantIsing.cavity_canonical_capped_log_bound line 40
  4. lemma OAI.InvariantIsing.integrable_cavity_canonical_capped_log line 56