OAI/Probability/InvariantIsing/Cavity/CavityHaarGibbsCappedReplica.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized fresh-Haar Gibbs comparison, with all ordinary-moment and strict finite-approximation assumptions proved for the actual models.

  1. theorem OAI.InvariantIsing.cavity_haar_gibbs_capped_replica_match line 16