OAI/Probability/InvariantIsing/Cavity/CavityReplicaCapFirstMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A first absolute energy moment suffices to remove the upper cap from bounded replica tests.

  1. lemma OAI.InvariantIsing.cavity_exp_cap_discard_first line 14
  2. lemma OAI.InvariantIsing.cavity_replica_cap_error_first line 37
  3. theorem OAI.InvariantIsing.cavity_replica_cap_mean_error_first line 70
  4. lemma OAI.InvariantIsing.cavity_replica_cap_expectation_error_first line 119