OAI/Probability/InvariantIsing/Cavity/CavityWindowMinimumLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite pressure minima imply the physical variational increment lower bound. No Gibbs-array limit is assumed here.

  1. theorem OAI.InvariantIsing.cavity_window_minimum_variational_lower line 17