OAI/Probability/InvariantIsing/Cavity/CavityGaussianCoordinateMap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite coordinate projection needed to select the physical special axes from the Gaussian spectral-group block.

  1. def OAI.InvariantIsing.cavityGaussianCoordinateMap line 16
  2. lemma OAI.InvariantIsing.cavity_gaussian_coordinate_hasGaussianLaw line 20
  3. lemma OAI.InvariantIsing.cavity_gaussian_coordinate_mean line 31
  4. theorem OAI.InvariantIsing.cavity_gaussian_coordinate_law line 48

    Source documentation

    Coordinate selection retains the corresponding covariance submatrix, including degenerate Gaussian laws.

    theorem cavity_gaussian_coordinate_law (S : Matrix I I ℝ) (hS : S.PosSemidef)
    (e : J → I) :
    (multivariateGaussian (0 : EuclideanSpace ℝ I) S).map (cavityGaussianCoordinateMap e) =
      multivariateGaussian 0 (S.submatrix e e) := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianCoordinateMap