OAI/Probability/InvariantIsing/Cavity/CavityReplicaCapTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cap removal from tightness of the full Gibbs law. Only the Gibbs mass of the set on which the energy cap acts enters the bound.

  1. lemma OAI.InvariantIsing.cavity_exp_cap_discard_tail line 14
  2. lemma OAI.InvariantIsing.cavity_replica_cap_tail_error line 35