OAI/Probability/InvariantIsing/Cavity/CavityHaarJointLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Random overlap labels and their fresh Haar marks converge jointly. The covariance is the actual finite replica Gram matrix, before taking the weak limit.

  1. theorem OAI.InvariantIsing.cavityGroupHaarFrame_joint_law_tendsto line 17