OAI/Probability/InvariantIsing/Magnetic/RestrictedCanonicalLogLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Identification of the canonical capped logarithm with the full original spin/leaf Gibbs probability and fresh spectral-group rotations.

  1. theorem OAI.InvariantIsing.restricted_canonical_capped_log_law line 16