OAI/Probability/InvariantIsing/Cavity/CavityReplicaGaussianAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded replica tests may be averaged over the actual Gaussian root and forest before, or after, sampling the labeled leaves.

  1. def OAI.InvariantIsing.cavityReplicaField line 14
  2. lemma OAI.InvariantIsing.measurable_cavityReplicaField line 22
  3. lemma OAI.InvariantIsing.cavity_replica_gaussian_test line 37
  4. theorem OAI.InvariantIsing.cavity_replica_gaussian_average line 53