OAI/Probability/InvariantIsing/Cavity/CavityLinearSpinEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the full linear cavity spin test under its independent Euclidean Gaussian forest and root. The covariance assumptions specify the scalar field path after projection.

  1. def OAI.InvariantIsing.cavityLinearFieldCoordinateLaw line 16
  2. def OAI.InvariantIsing.cavityLabeledLinearSpinPairMean line 23
  3. theorem OAI.InvariantIsing.cavity_labeled_linear_spin_pair_reduce line 39
  4. theorem OAI.InvariantIsing.cavity_labeled_linear_spin_pair_evaluation line 81