OAI/Probability/InvariantIsing/Cavity/CavityResidualIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full ordinary-residual exponential moment follows from the residual-free spin/leaf exponential moment.

  1. theorem OAI.InvariantIsing.cavity_residual_spin_exp_integrable line 14