OAI/Probability/InvariantIsing/Cavity/CavityUnflooredLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the positive floor after the bounded finite-replica passage. Only the second moment of the negative logarithm is used.

  1. lemma OAI.InvariantIsing.cavity_log_integrable_of_negative_sq line 14
  2. lemma OAI.InvariantIsing.cavity_floored_log_integrable line 29
  3. lemma OAI.InvariantIsing.cavity_log_floor_mean_difference line 43
  4. theorem OAI.InvariantIsing.cavity_unfloored_log_tendsto line 54