OAI/Probability/InvariantIsing/Cavity/CavitySpinReplicaMatch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual capped finite-spin replica moments under fresh Haar frames and under the recalculated Gaussian cascade. Spin integration is part of the bounded continuous test, so no spin law is inferred from weak convergence.

  1. theorem OAI.InvariantIsing.cavity_haar_capped_spin_replica_match line 15