OAI/Probability/InvariantIsing/Cavity/CavityGroupProjectionUniform.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniformity over all bounded spectral-group replica Gram arrays. This allows the fresh frames to be averaged against the base Gibbs measure.

  1. def OAI.InvariantIsing.cavityGroupReplicaGram line 14
  2. lemma OAI.InvariantIsing.cavityGroupReplicaGram_covariance line 19
  3. theorem OAI.InvariantIsing.cavityGroupHaarFrame_uniform_gaussian line 26