OAI/Probability/InvariantIsing/Cavity/CavityHaarProjection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Gaussian replica projections for genuine Haar-distributed orthonormal frames, obtained from the conditioned Gaussian construction.

  1. lemma OAI.InvariantIsing.cavityFrame_integral_eq_haar line 16
  2. def OAI.InvariantIsing.cavityMatrixProjection line 42
  3. lemma OAI.InvariantIsing.continuous_cavityMatrixProjection line 46
  4. theorem OAI.InvariantIsing.cavityHaarFrameProjection_integral_tendsto line 51