OAI/Probability/InvariantIsing/Cavity/CavityRandomCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A random cutoff changes bounded replica tests by its discarded one-replica probability, after averaging over the common disorder.

  1. lemma OAI.InvariantIsing.cavity_cutoff_replica_abs_le line 14
  2. theorem OAI.InvariantIsing.cavity_random_cutoff_error line 29