OAI/Probability/InvariantIsing/Cavity/CavityCanonicalSynchronization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The limiting Ward equations give the canonical monotone spectral labels on every off-diagonal entry, not only along quantile parameters.

  1. theorem OAI.InvariantIsing.cavity_canonical_group_synchronization line 15