OAI/Probability/InvariantIsing/Cavity/CavityPhysicalVariationalLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original physical model satisfies the finite-spectrum variational lower bound along a spectral/GG/Ward subsequence.

  1. theorem OAI.InvariantIsing.cavity_physical_variational_lower line 16