OAI/Probability/InvariantIsing/Magnetic/RestrictedRandomTreeLogLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The random-compression version of the canonical logarithmic law. The compression variable is independent of the base disorder and the fresh spectral-group rotations.

  1. theorem OAI.InvariantIsing.restricted_random_tree_log_law line 17