OAI/Probability/InvariantIsing/Cavity/CavityCappedLogLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic finite-replica passage with its floor removed. Fourth moments of the original marks control the negative logarithm.

  1. lemma OAI.InvariantIsing.cavity_capped_negative_log_mean_bound line 16
  2. theorem OAI.InvariantIsing.cavity_capped_log_limit line 47