Skip to content

Gaussian conditioning

DefinitionThe additive-noise kernel#✓fully proved

Let \(E\) be an additive commutative group with a measurable structure for which addition \(E \times E \to E\) is measurable, let \(F\) be a measurable space, let \(f \colon F \to E\) be a measurable map and let \(\nu\) be a measure on \(E\). If \(\nu\) is s-finite, the additive-noise kernel from \(F\) to \(E\) sends \(y \in F\) to the image of the product measure \(\delta_{f(y)} \otimes \nu\) (where \(\delta_{f(y)}\) is the Dirac measure at \(f(y)\)) under addition \((a, z) \mapsto a + z\), that is, to the image of \(\nu\) under \(z \mapsto f(y) + z\). If \(\nu\) is not s-finite, it is the zero kernel.

When \(\nu\) is a probability measure, the kernel sends \(y\) to the law of \(f(y) + Z\) for a random variable \(Z\) with law \(\nu\).

noncomputable def noiseKernel (f : F → E) (hf : Measurable f) (ν : Measure E) : Kernel F E :=
  (Kernel.deterministic f hf ×ₖ Kernel.const F ν).map fun p => p.1 + p.2
Used by 4
Used byConditioning on a signal observed in independent additive noise · Gaussian conditioning (Schur complement) · Gaussian conditioning · Conditional law of a Gaussian process at one time given another

TheoremConditioning on a signal observed in independent additive noise#✓fully proved

Let \(E\) be a nonempty standard Borel space that is an abelian group with measurable addition, let \(F\) be a measurable space, and let \(Y \colon \Omega \to F\) and \(Z \colon \Omega \to E\) be independent measurable random variables on a probability space. For every measurable \(f \colon F \to E\) and almost every \(y\) with respect to the law of \(Y\), the conditional distribution of \(f(Y) + Z\) given \(Y = y\) is the law of \(f(y) + Z\).

theorem condDistrib_add_of_indepFun [StandardBorelSpace E] [Nonempty E] {Y : Ω → F} {Z : Ω → E}
    (hY : Measurable Y) (hZ : Measurable Z) (hind : IndepFun Y Z P) {f : F → E}
    (hf : Measurable f) :
    condDistrib (fun ω => f (Y ω) + Z ω) Y P =ᵐ[P.map Y] noiseKernel f hf (P.map Z)
Uses 1 · Used by 1
Statement usesThe additive-noise kernel
Used byGaussian conditioning

TheoremGaussian conditioning#✓fully proved

Let \(E\) and \(F\) be finite-dimensional real inner product spaces, and let \(X\) and \(Y\) be measurable random vectors in \(E\) and \(F\) on a probability space such that \((X, Y)\) is jointly Gaussian. Let \(A \colon F \to E\) be a linear map whose residual \(X - A Y\) is uncorrelated with \(Y\) (the normal equations): for all \(u \in E\) and \(w \in F\), \(\operatorname{Cov}(\langle u, X - A Y \rangle, \langle w, Y \rangle) = 0\). Then \(X - A Y\) is Gaussian and independent of \(Y\), and for almost every \(y\) with respect to the law of \(Y\), the conditional distribution of \(X\) given \(Y = y\) is the law of \(A y + (X - A Y)\).

theorem condDistrib_of_hasGaussianLaw {X : Ω → E} {Y : Ω → F} (hX : Measurable X)
    (hY : Measurable Y) (hXY : HasGaussianLaw (fun ω => (X ω, Y ω)) P) (A : F →L[ℝ] E)
    (hA : ∀ x y, cov[fun ω => ⟪x, X ω - A (Y ω)⟫, fun ω => ⟪y, Y ω⟫; P] = 0) :
    HasGaussianLaw (fun ω => X ω - A (Y ω)) P ∧
      IndepFun (fun ω => X ω - A (Y ω)) Y P ∧
      condDistrib X Y P =ᵐ[P.map Y]
        noiseKernel A A.continuous.measurable (P.map fun ω => X ω - A (Y ω))
Uses 2 · Used by 2
Statement usesThe additive-noise kernel
Proof usesConditioning on a signal observed in independent additive noise
Used byGaussian conditioning (Schur complement) · Conditional law of a Gaussian process at one time given another

TheoremLinear images of multivariate Gaussians#✓fully proved

Write \(\mathcal{N}(a, \Sigma)\) for the multivariate Gaussian distribution with mean \(a\) and covariance matrix \(\Sigma\). Let \(\iota\) and \(\kappa\) be finite index sets, let \(M\) be a real \(\iota \times \kappa\) matrix, let \(\mu \in \mathbb{R}^\kappa\) and let \(S\) be a positive semidefinite real \(\kappa \times \kappa\) matrix. Then the image of \(\mathcal{N}(\mu, S)\) under the linear map \(z \mapsto M z\) is \(\mathcal{N}(M \mu, M S M^\top)\).

theorem map_toEuclideanLin_multivariateGaussian (M : Matrix ι κ ℝ) (μ : EuclideanSpace ℝ κ)
    {S : Matrix κ κ ℝ} (hS : S.PosSemidef) :
    (multivariateGaussian μ S).map (toEuclideanLin M) =
      multivariateGaussian (toEuclideanLin M μ) (M * S * Mᵀ)
Used by 4
Used byBLUP as a conditional law · Bayes' theorem for a linear-Gaussian observation · Gaussian conditioning (Schur complement) · The marginal of a linear-Gaussian model

TheoremTranslating a multivariate Gaussian#✓fully proved

Let \(\iota\) be a finite index set. For all \(c, \mu \in \mathbb{R}^\iota\) and every real \(\iota \times \iota\) matrix \(S\), the pushforward of \(N(\mu, S)\) under the translation \(x \mapsto c + x\) is \(N(c + \mu, S)\).

No positive semidefiniteness is assumed: when \(S\) is not positive semidefinite, \(N(\mu, S)\) is taken to be the point mass at \(\mu\).

theorem map_add_multivariateGaussian (c μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) :
    (multivariateGaussian μ S).map (c + ·) = multivariateGaussian (c + μ) S
Used by 2
Used byBLUP as a conditional law · Gaussian conditioning (Schur complement)

DefinitionHorizontal block matrix#✓fully proved

Let \(\rho\), \(\iota\) and \(\kappa\) be index sets with \(\iota\) and \(\kappa\) finite. For real matrices \(P\) with rows indexed by \(\rho\) and columns by \(\iota\), and \(Q\) with rows indexed by \(\rho\) and columns by \(\kappa\), the block row \([P\ Q]\) is the real matrix with rows indexed by \(\rho\) and columns indexed by the disjoint union \(\iota \sqcup \kappa\), whose entry in row \(r\) is \(P_{ri}\) in the column of \(i \in \iota\) and \(Q_{rk}\) in the column of \(k \in \kappa\).

def blockRow {ρ : Type*} (P : Matrix ρ ι ℝ) (Q : Matrix ρ κ ℝ) : Matrix ρ (ι ⊕ κ) ℝ :=
  Matrix.of fun r => Sum.elim (P r) (Q r)
Used by 8
Used byBLUP as a conditional law · The Gaussian-process posterior · Training-target projection · Test-value projection · Bayes' theorem for a linear-Gaussian observation · Gaussian conditioning (Schur complement) · The marginal of a linear-Gaussian model · Pairwise Markov property of Gaussian vectors

TheoremCovariances of linear functionals of a Gaussian vector#✓fully proved

Let \(\nu\) be a finite index set and let \(V\) be a measurable random vector in \(\mathbb{R}^\nu\) on a probability space with law \(N(\mu, S)\), where \(S\) is positive semidefinite. Then for all \(a, b \in \mathbb{R}^\nu\), \(\operatorname{Cov}(\langle a, V \rangle, \langle b, V \rangle) = a^\top S b\).

theorem covariance_inner_of_map_eq {ν : Type*} [Fintype ν] [DecidableEq ν]
    {V : Ω → EuclideanSpace ℝ ν} (hV : Measurable V) {μ : EuclideanSpace ℝ ν}
    {S : Matrix ν ν ℝ} (hS : S.PosSemidef) (hlaw : P.map V = multivariateGaussian μ S)
    (a b : EuclideanSpace ℝ ν) :
    cov[fun ω => ⟪a, V ω⟫, fun ω => ⟪b, V ω⟫; P] = ofLp a ⬝ᵥ S *ᵥ ofLp b
Used by 2
Used byGaussian conditioning (Schur complement) · Pairwise Markov property of Gaussian vectors

TheoremGaussian conditioning (Schur complement)#✓fully proved

Let \(\iota\) and \(\kappa\) be finite index sets and let \(V\) be a measurable random vector in \(\mathbb{R}^{\iota \sqcup \kappa}\) on a probability space, with blocks \(X \in \mathbb{R}^\iota\) and \(Y \in \mathbb{R}^\kappa\). Suppose \(V\) has law \(N(\mu, S)\) with \(S\) positive semidefinite, write \(\mu_X, \mu_Y\) for the blocks of \(\mu\) and \(S_{11}, S_{12}, S_{21}, S_{22}\) for the blocks of \(S\) indexed by \(\iota \times \iota\), \(\iota \times \kappa\), \(\kappa \times \iota\) and \(\kappa \times \kappa\), and suppose \(S_{22}\) is invertible. Then for almost every \(y\) with respect to the law of \(Y\), the conditional distribution of \(X\) given \(Y = y\) is \(N(\mu_X + S_{12} S_{22}^{-1} (y - \mu_Y), S_{11} - S_{12} S_{22}^{-1} S_{21})\).

theorem condDistrib_multivariateGaussian {V : Ω → EuclideanSpace ℝ (ι ⊕ κ)} (hV : Measurable V)
    {μ : EuclideanSpace ℝ (ι ⊕ κ)} {S : Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ} (hS : S.PosSemidef)
    (hlaw : P.map V = multivariateGaussian μ S) (hYY : IsUnit S.toBlocks₂₂.det) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin (blockRow (0 : Matrix κ ι ℝ) 1) (V ω)),
      condDistrib (fun ω => toEuclideanLin (blockRow (1 : Matrix ι ι ℝ) 0) (V ω))
          (fun ω => toEuclideanLin (blockRow (0 : Matrix κ ι ℝ) 1) (V ω)) P y =
        multivariateGaussian
          (toEuclideanLin (blockRow (1 : Matrix ι ι ℝ) 0) μ +
            toEuclideanLin (S.toBlocks₁₂ * S.toBlocks₂₂⁻¹)
              (y - toEuclideanLin (blockRow (0 : Matrix κ ι ℝ) 1) μ))
          (S.toBlocks₁₁ - S.toBlocks₁₂ * S.toBlocks₂₂⁻¹ * S.toBlocks₂₁)
Uses 6 · Used by 4
Statement usesHorizontal block matrix
Proof usesGaussian conditioning · Covariances of linear functionals of a Gaussian vector · Translating a multivariate Gaussian · Linear images of multivariate Gaussians · The additive-noise kernel
Used byBLUP as a conditional law · The Gaussian-process posterior · Bayes' theorem for a linear-Gaussian observation · Pairwise Markov property of Gaussian vectors
18 fully proved

Independent Gaussian blocks

TheoremBlock-diagonal matrices with positive semidefinite blocks#✓fully proved

Let \(\iota\) and \(\kappa\) be finite index sets and let \(S\) and \(R\) be positive semidefinite real matrices indexed by \(\iota\) and by \(\kappa\). Then the block-diagonal matrix \(\begin{pmatrix} S & 0 \\ 0 & R \end{pmatrix}\), indexed by \(\iota \sqcup \kappa\), is positive semidefinite.

theorem posSemidef_fromBlocks_zero [Finite ι] [Finite κ] {S : Matrix ι ι ℝ} {R : Matrix κ κ ℝ}
    (hS : S.PosSemidef) (hR : R.PosSemidef) : (fromBlocks S 0 0 R).PosSemidef
Used by 5
Used byBLUP as a conditional law · Bayes' theorem for a linear-Gaussian observation · The marginal of a linear-Gaussian model · Independent Gaussian blocks · The joint covariance of a linear-Gaussian model is positive semidefinite

TheoremThe inner product splits over blocks#✓fully proved

Let \(\iota\) and \(\kappa\) be finite index sets. For \(p_1 \in \mathbb{R}^\iota\), \(p_2 \in \mathbb{R}^\kappa\) and \(t \in \mathbb{R}^{\iota \sqcup \kappa}\) with blocks \(t_\iota \in \mathbb{R}^\iota\) and \(t_\kappa \in \mathbb{R}^\kappa\), the inner product of the concatenation of \(p_1\) and \(p_2\) with \(t\) is \(\langle p_1, t_\iota \rangle + \langle p_2, t_\kappa \rangle\).

theorem inner_sumEquivProd_symm (p : EuclideanSpace ℝ ι × EuclideanSpace ℝ κ)
    (t : EuclideanSpace ℝ (ι ⊕ κ)) :
    ⟪(EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm p, t⟫ =
      ⟪p.1, (EuclideanSpace.sumEquivProd (𝕜 := ℝ) t).1⟫ +
        ⟪p.2, (EuclideanSpace.sumEquivProd (𝕜 := ℝ) t).2⟫
Used by 2
Used byCharacteristic function of a product of blocks · Independent Gaussian blocks

TheoremCharacteristic function of a product of blocks#✓fully proved

Let \(\iota\) and \(\kappa\) be finite index sets, let \(\mu\) and \(\nu\) be finite measures on \(\mathbb{R}^\iota\) and \(\mathbb{R}^\kappa\), and let \(\pi\) be the pushforward of the product measure \(\mu \otimes \nu\) to \(\mathbb{R}^{\iota \sqcup \kappa}\) under concatenation of the two blocks. Write \(\varphi_\rho\) for the characteristic function of a measure \(\rho\). Then for every \(t \in \mathbb{R}^{\iota \sqcup \kappa}\) with blocks \(t_\iota \in \mathbb{R}^\iota\) and \(t_\kappa \in \mathbb{R}^\kappa\), we have \(\varphi_\pi(t) = \varphi_\mu(t_\iota) \, \varphi_\nu(t_\kappa)\).

theorem charFun_map_sumEquivProd_symm_prod (μ : Measure (EuclideanSpace ℝ ι))
    (ν : Measure (EuclideanSpace ℝ κ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (t : EuclideanSpace ℝ (ι ⊕ κ)) :
    charFun ((μ.prod ν).map (EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm) t =
      charFun μ (EuclideanSpace.sumEquivProd (𝕜 := ℝ) t).1 *
        charFun ν (EuclideanSpace.sumEquivProd (𝕜 := ℝ) t).2
Uses 1 · Used by 1
Proof usesThe inner product splits over blocks
Used byIndependent Gaussian blocks

TheoremIndependent Gaussian blocks#✓fully proved

Write \(\mathcal{N}(a, \Sigma)\) for the multivariate Gaussian distribution with mean \(a\) and covariance matrix \(\Sigma\). Let \(\iota\) and \(\kappa\) be finite index sets, let \(m \in \mathbb{R}^\iota\) and \(m' \in \mathbb{R}^\kappa\), and let \(S\) and \(R\) be positive semidefinite real matrices indexed by \(\iota\) and by \(\kappa\). Then the image of the product measure \(\mathcal{N}(m, S) \otimes \mathcal{N}(m', R)\) under the concatenation map \(\mathbb{R}^\iota \times \mathbb{R}^\kappa \to \mathbb{R}^{\iota \sqcup \kappa}\) is \(\mathcal{N}\left((m, m'), \begin{pmatrix} S & 0 \\ 0 & R \end{pmatrix}\right)\).

theorem map_sumEquivProd_symm_prod_multivariateGaussian (m : EuclideanSpace ℝ ι)
    (m' : EuclideanSpace ℝ κ) {S : Matrix ι ι ℝ} {R : Matrix κ κ ℝ} (hS : S.PosSemidef)
    (hR : R.PosSemidef) :
    ((multivariateGaussian m S).prod (multivariateGaussian m' R)).map
        (EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm =
      multivariateGaussian ((EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm (m, m'))
        (fromBlocks S 0 0 R)
Uses 3 · Used by 1
Proof usesCharacteristic function of a product of blocks · The inner product splits over blocks · Block-diagonal matrices with positive semidefinite blocks
Used byConcatenation of independent Gaussian random vectors

TheoremConcatenation of independent Gaussian random vectors#✓fully proved

Write \(\mathcal{N}(a, \Sigma)\) for the multivariate Gaussian distribution with mean \(a\) and covariance matrix \(\Sigma\). Let \(\iota\) and \(\kappa\) be finite index sets, and let \(x\) and \(v\) be independent measurable random vectors in \(\mathbb{R}^\iota\) and \(\mathbb{R}^\kappa\) on a probability space, with laws \(\mathcal{N}(m, S)\) and \(\mathcal{N}(m', R)\) for positive semidefinite real matrices \(S\) and \(R\). Then the concatenated random vector \((x, v)\) in \(\mathbb{R}^{\iota \sqcup \kappa}\) has law \(\mathcal{N}\left((m, m'), \begin{pmatrix} S & 0 \\ 0 & R \end{pmatrix}\right)\).

theorem map_sumEquivProd_symm_of_indepFun {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    [IsProbabilityMeasure P] {x : Ω → EuclideanSpace ℝ ι} {v : Ω → EuclideanSpace ℝ κ}
    (hx : Measurable x) (hv : Measurable v) (hind : IndepFun x v P) {m : EuclideanSpace ℝ ι}
    {m' : EuclideanSpace ℝ κ} {S : Matrix ι ι ℝ} {R : Matrix κ κ ℝ} (hS : S.PosSemidef)
    (hR : R.PosSemidef) (hxl : P.map x = multivariateGaussian m S)
    (hvl : P.map v = multivariateGaussian m' R) :
    P.map (fun ω => (EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm (x ω, v ω)) =
      multivariateGaussian ((EuclideanSpace.sumEquivProd (𝕜 := ℝ)).symm (m, m'))
        (fromBlocks S 0 0 R)
Uses 1 · Used by 3
Proof usesIndependent Gaussian blocks
Used byBLUP as a conditional law · Bayes' theorem for a linear-Gaussian observation · The marginal of a linear-Gaussian model

Linear-Gaussian models: marginals and Bayes' theorem

TheoremBlock-triangular congruence of a block-diagonal matrix#✓fully proved

Let \(n\) and \(p\) be finite index sets and let \(S\), \(R\) and \(H\) be real matrices of sizes \(n \times n\), \(p \times p\) and \(p \times n\). Let \(M\) be the block matrix with block rows \((I_n, 0)\) and \((H, I_p)\), and let \(D\) be the block-diagonal matrix with diagonal blocks \(S\) and \(R\). Then \(M D M^\top\) is the block matrix with block rows \((S, S H^\top)\) and \((H S, H S H^\top + R)\).

When \(x\) and \(v\) are independent random vectors with covariances \(S\) and \(R\), this is the joint covariance of \((x, H x + v)\).

theorem fromBlocks_one_zero_mul_mul_transpose (S : Matrix n n ℝ) (R : Matrix p p ℝ)
    (H : Matrix p n ℝ) :
    fromBlocks 1 0 H 1 * fromBlocks S 0 0 R * (fromBlocks 1 0 H 1)ᵀ =
      fromBlocks S (S * Hᵀ) (H * S) (H * S * Hᵀ + R)
Used by 3
Used byBLUP as a conditional law · Bayes' theorem for a linear-Gaussian observation · The joint covariance of a linear-Gaussian model is positive semidefinite

TheoremThe joint covariance of a linear-Gaussian model is positive semidefinite#✓fully proved

Let \(n\) and \(p\) be finite index sets, let \(S\) and \(R\) be positive semidefinite real matrices indexed by \(n\) and by \(p\), and let \(H\) be a real \(p \times n\) matrix. Then the block matrix \(\begin{pmatrix} S & S H^\top \\ H S & H S H^\top + R \end{pmatrix}\), indexed by \(n \sqcup p\), is positive semidefinite.

theorem posSemidef_fromBlocks_linear [Finite p] {S : Matrix n n ℝ} {R : Matrix p p ℝ}
    (hS : S.PosSemidef) (hR : R.PosSemidef) (H : Matrix p n ℝ) :
    (fromBlocks S (S * Hᵀ) (H * S) (H * S * Hᵀ + R)).PosSemidef
Uses 2 · Used by 3
Proof usesBlock-triangular congruence of a block-diagonal matrix · Block-diagonal matrices with positive semidefinite blocks
Used byBLUP as a conditional law · Bayes' theorem for a linear-Gaussian observation · The posterior covariance is positive semidefinite

TheoremThe posterior covariance is positive semidefinite#✓fully proved

Let \(n\) and \(p\) be finite index sets, let \(S\) be a positive semidefinite real \(n \times n\) matrix, let \(R\) be a positive definite real \(p \times p\) matrix and let \(H\) be a real \(p \times n\) matrix. Then \(S - S H^\top (H S H^\top + R)^{-1} H S\) is positive semidefinite.

This matrix is the Schur complement of the lower-right block in the joint covariance \(\begin{pmatrix} S & S H^\top \\ H S & H S H^\top + R \end{pmatrix}\) of a linear-Gaussian model.

theorem posSemidef_sub_mul_inv_mul {S : Matrix n n ℝ} {R : Matrix p p ℝ} (hS : S.PosSemidef)
    (hR : R.PosDef) (H : Matrix p n ℝ) :
    (S - S * Hᵀ * (H * S * Hᵀ + R)⁻¹ * (H * S)).PosSemidef
Uses 1 · Used by 1
Proof usesThe joint covariance of a linear-Gaussian model is positive semidefinite
Used byThe Kalman update preserves validity

TheoremThe marginal of a linear-Gaussian model#✓fully proved

Write \(\mathcal{N}(a, \Sigma)\) for the multivariate Gaussian distribution with mean \(a\) and covariance matrix \(\Sigma\). Let \(n\) and \(p\) be finite index sets, and let \(x\) and \(w\) be independent measurable random vectors in \(\mathbb{R}^n\) and \(\mathbb{R}^p\) on a probability space, where \(x\) has law \(\mathcal{N}(m, S)\) and \(w\) has law \(\mathcal{N}(c, Q)\) for positive semidefinite real matrices \(S\) and \(Q\). Then for every real \(p \times n\) matrix \(F\), the random vector \(F x + w\) has law \(\mathcal{N}(F m + c, F S F^\top + Q)\).

theorem map_linear_add_of_indepFun {x : Ω → EuclideanSpace ℝ n} {w : Ω → EuclideanSpace ℝ p}
    (hx : Measurable x) (hw : Measurable w) (hind : IndepFun x w P) {m : EuclideanSpace ℝ n}
    {c : EuclideanSpace ℝ p} {S : Matrix n n ℝ} {Q : Matrix p p ℝ} (hS : S.PosSemidef)
    (hQ : Q.PosSemidef) (hxl : P.map x = multivariateGaussian m S)
    (hwl : P.map w = multivariateGaussian c Q) (F : Matrix p n ℝ) :
    P.map (fun ω => toEuclideanLin F (x ω) + w ω) =
      multivariateGaussian (toEuclideanLin F m + c) (F * S * Fᵀ + Q)
Uses 4 · Used by 2
Proof usesHorizontal block matrix · Concatenation of independent Gaussian random vectors · Linear images of multivariate Gaussians · Block-diagonal matrices with positive semidefinite blocks
Used byThe marginal law of the phenotype given the causal variant · The predict step is exact

TheoremBayes' theorem for a linear-Gaussian observation#✓fully proved

Let \(n\) and \(p\) be finite index sets, and let \(x\) and \(v\) be independent measurable random vectors in \(\mathbb{R}^n\) and \(\mathbb{R}^p\) on a probability space, with \(x \sim N(m, S)\) and \(v \sim N(0, R)\) for positive semidefinite matrices \(S\) and \(R\). Let \(H\) be a real \(p \times n\) matrix such that \(H S H^\top + R\) is invertible, and let \(Y = H x + v\). Then for almost every \(y\) with respect to the law of \(Y\), the conditional distribution of \(x\) given \(Y = y\) is the Gaussian with mean \(m + S H^\top (H S H^\top + R)^{-1} (y - H m)\) and covariance \(S - S H^\top (H S H^\top + R)^{-1} H S\).

theorem condDistrib_linear_add_of_indepFun {x : Ω → EuclideanSpace ℝ n}
    {v : Ω → EuclideanSpace ℝ p} (hx : Measurable x) (hv : Measurable v) (hind : IndepFun x v P)
    {m : EuclideanSpace ℝ n} {S : Matrix n n ℝ} {R : Matrix p p ℝ} (hS : S.PosSemidef)
    (hR : R.PosSemidef) (hxl : P.map x = multivariateGaussian m S)
    (hvl : P.map v = multivariateGaussian 0 R) (H : Matrix p n ℝ)
    (hinv : IsUnit (H * S * Hᵀ + R).det) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin H (x ω) + v ω),
      condDistrib x (fun ω => toEuclideanLin H (x ω) + v ω) P y =
        multivariateGaussian
          (m + toEuclideanLin (S * Hᵀ * (H * S * Hᵀ + R)⁻¹) (y - toEuclideanLin H m))
          (S - S * Hᵀ * (H * S * Hᵀ + R)⁻¹ * (H * S))
Uses 7 · Used by 3
Proof usesHorizontal block matrix · Gaussian conditioning (Schur complement) · Block-triangular congruence of a block-diagonal matrix · Concatenation of independent Gaussian random vectors · Linear images of multivariate Gaussians · The joint covariance of a linear-Gaussian model is positive semidefinite · Block-diagonal matrices with positive semidefinite blocks
Used byThe LDpred-inf posterior · The effect posterior of the single-effect regression · The update step is the exact posterior

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.