OAI/Probability/InvariantIsing/Cavity/CavityVariationalTrialLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing from the convergent physical entropy trial to the finite spectral variational lower bound.

  1. theorem OAI.InvariantIsing.cavity_variational_lower_of_trial_limit line 14