OAI/Probability/InvariantIsing/Cavity/CavityOneReplicaGaussian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian marginal of a single sampled innovation leaf and its residual.

  1. theorem OAI.InvariantIsing.cavity_marked_leaf_sum_law line 14
  2. theorem OAI.InvariantIsing.cavity_marked_leaf_residual_law line 33