OAI/Probability/InvariantIsing/Cavity/CavityMultivariateGaussian.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The quadratic integral for the actual multivariate Gaussian law. The covariance is allowed to be singular.

  1. lemma OAI.InvariantIsing.cavity_covariance_sqrt_factor line 15
  2. theorem OAI.InvariantIsing.cavity_multivariate_gaussian_integrable line 25
  3. theorem OAI.InvariantIsing.cavity_multivariate_gaussian_integral line 39

    Source documentation

    The exact covariance form of cav:q-factor, with no inverse of the covariance and hence no nondegeneracy assumption on it.

    theorem cavity_multivariate_gaussian_integral {d : ℕ}
    (K S : Matrix (Fin d) (Fin d) ℝ) (hK : K.IsHermitian) (hS : S.PosSemidef)
    (hQ : (cavityFactorPrecision K (CFC.sqrt S)).PosDef)
    (u : EuclideanSpace ℝ (Fin d)) :
    (∫ z : EuclideanSpace ℝ (Fin d),
      Real.exp (⟪u + z, Matrix.toEuclideanCLM (𝕜 := ℝ) K (u + z)⟫ / 2)
…

    Mentions: OAI.InvariantIsing.cavityFactorPrecision

  4. theorem OAI.InvariantIsing.cavity_multivariate_gaussian_logIntegral line 53