OAI/Probability/InvariantIsing/Cavity/CavityEntropyMaximum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identification of the entropy in the cavity limit. Approximate self-consistency, with the actual scalar supporting inequality, makes the finite field trials approach the entropy supremum.

  1. theorem OAI.InvariantIsing.field_entropy_sequence line 19
  2. theorem OAI.InvariantIsing.cavity_entropy_trial_tendsto line 30
  3. theorem OAI.InvariantIsing.cavity_entropy_trial_eventually_lower line 57