OAI/Probability/InvariantIsing/Cavity/CavityFiniteEvaluation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar-spin and quadratic parts of the finite cavity calculation combine to the variational trial value, with the residual Gaussian integrated as an ordinary expectation.

  1. theorem OAI.InvariantIsing.cavity_finite_spin_quadratic_value line 17