OAI/Probability/InvariantIsing/Cavity/CavityFrameTransitive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ambient orthogonal group acts transitively on finite orthonormal frames. This identifies the orbit on which the conditioned Gaussian frame law will be compared with Haar measure.

  1. theorem OAI.InvariantIsing.cavity_orthonormal_transitive line 14