OAI/Probability/InvariantIsing/Cavity/CavityLogProbability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A concentrating quadratic coefficient error may be removed from the expected capped logarithm without an inverse-normalizer assumption.

  1. theorem OAI.InvariantIsing.cavity_capped_log_probability_limit line 15