ExampleConstruction: Literature-sourcedVerification: 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.

Full conditionals for a bivariate normal target

Example

Assume AC. Let $- 1 < ρ < 1$ and let $π = N_{2} (0, Σ_{ρ})$ on $R^{2}$ , where $Σ_{ρ} = (\begin{array}{cc} 1 & ρ \\ ρ & 1 \end{array}) .$ Writing the state as $(X, Y)$ , its proper full conditionals are $X ∣ Y = y \sim N (ρ y, 1 - ρ^{2}), Y ∣ X = x \sim N (ρ x, 1 - ρ^{2}) (x, y \in R) .$ The variances are positive for every allowed $ρ$ , so each conditional is a pointwise probability kernel on the whole conditioning space. A systematic scan that updates $X$ and then $Y$ can be run by the two corresponding updates of Exact Gibbs block update.

Facts & Assumptions

Given: AC, $- 1 < ρ < 1$ , and the target law in the Example.

[F1]

For a nondegenerate bivariate normal target, both pointwise proper full conditionals are normal with the displayed conditional means and variances. Proper full conditionals of a nondegenerate bivariate normal law.

[A1]

AC is the stated premise of the bivariate-normal conditional-density supplier and its normal-law convention. The Axiom of Choice.

[F2]

A Gibbs block update keeps the retained coordinate and samples the updated coordinate from its supplied full conditional kernel. Exact Gibbs block update.

Verification

Given: The hypotheses in the Example and facts [A1], [F1], [F2].

1.1A1F1given

Apply [F1] with $m_{X} = m_{Y} = 0$ , $σ_{X} = σ_{Y} = 1$ , and $r = ρ$ . This gives $X ∣ Y = y \sim N (ρ y, 1 - ρ^{2})$ for every $y$ . Applying the same supplier with the coordinates exchanged gives $Y ∣ X = x \sim N (ρ x, 1 - ρ^{2})$ for every $x$ . Since $1 - ρ^{2} > 0$ , both laws are nondegenerate normal probabilities, and the supplier gives their normalized densities as everywhere conditional kernels.

2.1F1F2given∎

With these two kernels, [F2] updates $X$ by drawing from the first conditional while holding $Y$ fixed, and then updates $Y$ from the second conditional at the new $X$ value. Both are exact block updates for the stated target, with no support or zero-normalizer exception because the conditional variances are strictly positive.

Depends on

Used by

A systematic Gaussian Gibbs sweep need not be reversible Example

Dependency tree · two levels

20 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)