OAI/Probability/InvariantIsing/Cavity/CavityConcreteHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual measurable finite cavity construction has a Haar base spectral orbit independent of its compression matrices.

  1. theorem OAI.InvariantIsing.cavityConcreteBase_haar_factorization line 15