OAI/Probability/InvariantIsing/Cavity/CavityHaarSpinNumerator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Product-disorder integration for physical Haar spin numerators.

  1. lemma OAI.InvariantIsing.cavity_haar_spin_replica_integral line 14
  2. lemma OAI.InvariantIsing.cavity_haar_spin_numerator_integral line 47
  3. lemma OAI.InvariantIsing.cavity_group_gram_diagonal_norm line 85