OAI/Probability/InvariantIsing/Cavity/CavityGaussianFactor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Quadratic Gaussian integration through an arbitrary covariance factor. The factor may be singular and need not commute with K.

  1. lemma OAI.InvariantIsing.cavity_matrix_transpose_inner line 15
  2. def OAI.InvariantIsing.cavityFactorLinear line 22
  3. lemma OAI.InvariantIsing.cavity_factor_precision_quadratic line 26
  4. lemma OAI.InvariantIsing.cavity_factor_linear_inner line 36
  5. lemma OAI.InvariantIsing.cavity_factor_exponent line 51
  6. lemma OAI.InvariantIsing.cavity_factor_exponential line 66
  7. lemma OAI.InvariantIsing.cavity_factor_completed_quadratic line 75
  8. theorem OAI.InvariantIsing.cavity_gaussian_factor_integrable line 90
  9. theorem OAI.InvariantIsing.cavity_gaussian_factor_integral line 102

    Source documentation

    Square completion with covariance B Bᵀ, including singular factors.

    theorem cavity_gaussian_factor_integral {d : ℕ}
    (K B : Matrix (Fin d) (Fin d) ℝ) (hK : K.IsHermitian)
    (hQ : (cavityFactorPrecision K B).PosDef) (u : EuclideanSpace ℝ (Fin d)) :
    (∫ z : EuclideanSpace ℝ (Fin d),
      Real.exp (⟪u + Matrix.toEuclideanCLM (𝕜 := ℝ) B z,
…

    Mentions: OAI.InvariantIsing.cavityFactorPrecision