OAI/Probability/InvariantIsing/Cavity/CavityLogFloor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform second moment of the negative log normalizer permits removing the positive floor after the finite-replica limit.

  1. lemma OAI.InvariantIsing.cavity_log_floor_bound line 14
  2. lemma OAI.InvariantIsing.cavity_log_floor_integral_bound line 52
  3. lemma OAI.InvariantIsing.cavity_log_floor_uniform line 82