CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Proper full conditionals of a nondegenerate bivariate normal law

Statement

Assume AC. Let $m_{X}, m_{Y} \in R$ , let $σ_{X}, σ_{Y} > 0$ , and let $- 1 < r < 1$ . Put $Σ = (\begin{array}{cc} σ_{X}^{2} & r σ_{X} σ_{Y} \\ r σ_{X} σ_{Y} & σ_{Y}^{2} \end{array}), π = N_{2} ((m_{X}, m_{Y}), Σ) .$ Then proper full conditional kernels of $X$ given $Y = y$ and of $Y$ given $X = x$ , at every real conditioning value, are $X ∣ Y = y \sim N ⁣ (m_{X} + r \frac{σ_{X}}{σ_{Y}} (y - m_{Y}), σ_{X}^{2} (1 - r^{2})), Y ∣ X = x \sim N ⁣ (m_{Y} + r \frac{σ_{Y}}{σ_{X}} (x - m_{X}), σ_{Y}^{2} (1 - r^{2})) .$ Both conditional variances are strictly positive. The singular cases $∣ r ∣ = 1$ are not included.

Facts & Assumptions

Given: AC, the real parameters and strict inequalities in the Statement, and the target law $π$ .

[A1]

AC implies countable choice, which is the choice assumption required by the nonnegative change-of-variables theorem. The Axiom of Choice, AC supplies countable selections and prescribed serial paths.

[F1]

A multivariate normal law has the specified mean and covariance matrix, under the library's projection-law convention. Multivariate normal law, including singular covariance.

[F2]

For a positive-definite covariance matrix, $N_{2}$ has density $(2 π)^{- 1} \det (Σ)^{- 1 / 2} \exp [- \frac{1}{2} (z - m)^{T} Σ^{- 1} (z - m)]$ . A positive-definite multivariate normal law has its Gaussian density.

[F3]

Product Lebesgue measure on $R \times R$ agrees with Euclidean Lebesgue measure on Borel sets. On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}.

[F4]

Under countable choice, a $C^{1}$ diffeomorphism obeys change of variables for every nonnegative Lebesgue-measurable integrand. A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions.

[F5]

The standard normal has density $ϕ (t) = (2 π)^{- 1 / 2} e^{- t^{2} / 2}$ , and $N (a, s^{2})$ is the law of $t \mapsto a + s t$ for $s > 0$ . Standard normal and normal laws.

[F6]

Multiplication of a nonnegative integrand by a positive finite scalar multiplies its integral by that scalar. Monotonicity and nonnegative homogeneity of the nonnegative integral.

[F7]

A joint density with a supplied probability filler yields an everywhere probability full-conditional kernel, with the conditional event identities. A joint density supplies a proper full conditional kernel.

[F8]

Proper full conditional means a pointwise probability kernel satisfying the block conditional event identity. Proper full conditional kernel.

Proof

Given: The hypotheses in the Statement and facts [A1], [F1]–[F8].

1.1A1F1F2F3algebra

Write $u = (x - m_{X}) / σ_{X}$ and $v = (y - m_{Y}) / σ_{Y}$ . The quadratic form of $Σ$ is $(a, b) Σ (a, b)^{T} = (σ_{X} a + r σ_{Y} b)^{2} + (1 - r^{2}) σ_{Y}^{2} b^{2}$ , so it is positive for every nonzero $(a, b)$ ; also $\det Σ = σ_{X}^{2} σ_{Y}^{2} (1 - r^{2}) > 0$ . Its inverse is $Σ^{- 1} = \frac{1}{σ_{X}^{2} σ_{Y}^{2} (1 - r^{2})} (\begin{array}{cc} σ_{Y}^{2} & - r σ_{X} σ_{Y} \\ - r σ_{X} σ_{Y} & σ_{X}^{2} \end{array})$ . Thus [F2] applies. Substitution into its density formula, using [F3] to identify the product reference measure, gives $p (x, y) = \frac{1}{2 π σ_{X} σ_{Y} \sqrt{1 - r^{2}}} \exp [- \frac{u^{2} - 2 r u v + v^{2}}{2 (1 - r^{2})}]$ . The covariance convention in [F1] fixes the parameters used here.

2.1F2step 1.1algebra

Set $s_{X} = σ_{X} \sqrt{1 - r^{2}}$ , $s_{Y} = σ_{Y} \sqrt{1 - r^{2}}$ , $a (y) = m_{X} + r σ_{X} v$ , and $b (x) = m_{Y} + r σ_{Y} u$ . For $s > 0$ write $g_{c, s} (t) = s^{- 1} ϕ ((t - c) / s)$ . The identities $u^{2} - 2 r u v + v^{2} = (u - r v)^{2} + (1 - r^{2}) v^{2} = (v - r u)^{2} + (1 - r^{2}) u^{2}$ therefore give both factorizations $p (x, y) = g_{m_{Y}, σ_{Y}} (y) g_{a (y), s_{X}} (x) = g_{m_{X}, σ_{X}} (x) g_{b (x), s_{Y}} (y)$ . Expanding each squared term verifies the exponents, and multiplying the factors verifies the prefactors.

3.1A1F4F5F6step 2.1

For any $c \in R$ , $s > 0$ , and Borel set $A \subseteq R$ , the diffeomorphism $T (t) = c + s t$ in [F4] gives $\int_{A} g_{c, s} (z) d z = \int_{T^{- 1} (A)} ϕ (t) d t = N (c, s^{2}) (A)$ by [F5]. Thus each $g_{c, s}$ is a probability density. Applying [F6] to the first factorization in step 2.1 yields $m_{Y} (y) = \int p (x, y) d x = g_{m_{Y}, σ_{Y}} (y)$ ; the second factorization gives $m_{X} (x) = \int p (x, y) d y = g_{m_{X}, σ_{X}} (x)$ . These marginal densities are finite and strictly positive at every real argument.

4.1F5F7F8step 2.1step 3.1algebra∎

Apply [F7] to $p$ with Lebesgue reference measures and, for each updated coordinate, the supplied filler $N (0, 1)$ from [F5]. Since both marginal densities in step 3.1 are finite and positive everywhere, the density formula is used on every conditioning fibre. For measurable $A \subseteq R$ , the first conditional kernel is $K_{X} (y, A) = \frac{\int_{A} p (x, y) d x}{m_{Y} (y)} = \int_{A} g_{a (y), s_{X}} (x) d x = N (a (y), s_{X}^{2}) (A)$ , using the factorization in step 2.1 and density identification in step 3.1. Exchanging coordinates gives $K_{Y} (x, A) = N (b (x), s_{Y}^{2}) (A)$ . By [F7] these are probability kernels satisfying the conditional event identities; [F8] identifies them as proper full conditionals at every conditioning value. The proof makes no assertion at the excluded singular endpoints.

Depends on

Used by

Full conditionals for a bivariate normal target Example

Dependency tree · two levels

60 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 12 (standard reference, not scraped)
Gareth O. Roberts and Jeffrey S. Rosenthal, General State Space Markov Chains and MCMC Algorithms (standard reference, not scraped)