OAI/Probability/InvariantIsing/Cavity/CavityGroupGaussian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Independent Gaussian arrays for the finitely many spectral groups. The finite restrictions are exactly standard Gaussian vectors.

  1. def OAI.InvariantIsing.cavityGroupGaussianRows line 14
  2. instance OAI.InvariantIsing.(instance at line 17) line 17
  3. lemma OAI.InvariantIsing.cavityGroupGaussian_eval_law line 20
  4. lemma OAI.InvariantIsing.cavityGroupGaussian_row_law line 26
  5. lemma OAI.InvariantIsing.cavityGroupGaussian_coordinate_law line 31
  6. lemma OAI.InvariantIsing.cavityGroupGaussian_coordinates_independent line 36
  7. lemma OAI.InvariantIsing.cavityGroupGaussian_finite_array_law line 51
  8. theorem OAI.InvariantIsing.cavityGroupGaussian_finite_standard_law line 70