OAI/Probability/InvariantIsing/Core/FiniteSpinEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy and the log-sum variational bound used to project canonical spins onto an attainable constrained block. Zero trial masses are allowed and contribute zero.

  1. def OAI.InvariantIsing.finiteShannonEntropy line 14
  2. lemma OAI.InvariantIsing.finite_relativeEntropy_nonneg_of_sum_le line 17
  3. lemma OAI.InvariantIsing.finite_relativeEntropy_nonneg line 36
  4. def OAI.InvariantIsing.finiteCanonicalWeights line 42
  5. lemma OAI.InvariantIsing.finiteCanonicalWeights_pos line 45
  6. lemma OAI.InvariantIsing.finiteCanonicalWeights_sum line 49
  7. lemma OAI.InvariantIsing.log_sum_exp_ge_trial line 54
  8. lemma OAI.InvariantIsing.log_sum_exp_eq_canonical line 71