OAI/Probability/InvariantIsing/Cavity/CavityHaarGibbsCappedLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Capped logarithmic limits for the actual fresh-Haar Gibbs model, from the spectral/GG limit and the derived ordinary moment bounds.

  1. theorem OAI.InvariantIsing.cavity_haar_gibbs_capped_log_match line 16