OAI/Probability/InvariantIsing/Cavity/CavityPriorEndpointLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed labeled path, its common Gaussian root, and its independent ordinary residual have the full unweighted endpoint covariance.

  1. lemma OAI.InvariantIsing.cavity_forest_leaf_sum_law line 15
  2. lemma OAI.InvariantIsing.cavity_root_forest_leaf_law line 29
  3. lemma OAI.InvariantIsing.cavity_prior_endpoint_law line 49