OAI/Probability/InvariantIsing/Cavity/CavityHaarModelNumerator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Physical fresh-Haar capped spin moments converge to the actual finite labeled cavity model, with all strict approximation premises derived.

  1. theorem OAI.InvariantIsing.cavity_haar_model_numerator_match line 15