OAI/Probability/InvariantIsing/Cavity/CavityProjectorJointHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint factorization allows the replica test to depend on the actual compression coefficients, not only through a separate scalar factor.

  1. theorem OAI.InvariantIsing.cavity_labeled_projector_joint_haar line 15