OAI/Probability/InvariantIsing/Cavity/CavityGroupHaarProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The joint Gaussian projection limit for independent Haar frames in all spectral groups. The exact finite-dimensional law is obtained before taking limits; no conditional independence is assumed as an extra input.

  1. lemma OAI.InvariantIsing.cavityGoodGram_cond_eq line 16
  2. lemma OAI.InvariantIsing.cavityGaussianNormalizedFrame_eq_haar line 23
  3. def OAI.InvariantIsing.cavityGroupNormalizedFrames line 36
  4. def OAI.InvariantIsing.cavityGroupHaarFrames line 40
  5. lemma OAI.InvariantIsing.measurable_cavityGroupNormalizedFrames line 45
  6. lemma OAI.InvariantIsing.continuous_cavityGroupHaarFrames line 50
  7. lemma OAI.InvariantIsing.measurable_cavityGroupHaarFrames line 60
  8. theorem OAI.InvariantIsing.cavityGroupNormalizedFrames_eq_haar line 68
  9. def OAI.InvariantIsing.cavityGroupMatrixProjection line 85
  10. lemma OAI.InvariantIsing.continuous_cavityGroupMatrixProjection line 91
  11. lemma OAI.InvariantIsing.cavityGroupFrame_integral_eq_haar line 97
  12. theorem OAI.InvariantIsing.cavityGroupHaarFrameProjection_integral_tendsto line 118