OAI/Probability/InvariantIsing/Cavity/CavityFiniteGaussian.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-dimensional laws of the independent Gaussian array used in the fresh-frame construction.

  1. lemma OAI.InvariantIsing.cavityGaussianRows_coordinate_law line 14
  2. lemma OAI.InvariantIsing.cavityGaussianRows_coordinates_independent line 19
  3. lemma OAI.InvariantIsing.cavityGaussianRows_finite_array_law line 26
  4. theorem OAI.InvariantIsing.cavityGaussianRows_finite_standard_law line 43