OAI/Probability/InvariantIsing/Cavity/CavityLabeledModelIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exponential integrability of the literal finite labeled cavity model, derived from the Gaussian quadratic calculation on the original model.

  1. theorem OAI.InvariantIsing.cavity_labeled_model_integrability line 15