LemmaStatement: 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.

A Gibbs refresh is conditionally independent of the old block

Statement

Assume AC for the conditional-expectation class convention in Conditional independence given a sigma-algebra. Let $X = (U, Z)$ have law $π$ , where $U$ is the block $B$ and $Z$ is the retained coordinate. Update once using Exact Gibbs block update, and write $V$ for the refreshed block. Under the resulting joint law of $(U, Z, V)$ , $U ⊥ ⁣ ⁣ ⁣ ⊥ V ∣ σ (Z) .$ Both $U$ and $V$ have conditional law $K_{B} (Z, \cdot)$ given $Z$ .

Facts & Assumptions

Given: A target probability $π$ , a supplied proper full conditional kernel $K_{B}$ , and one exact block update.

[A1]

AC supplies the library's conditional-expectation class convention used by the conditional-independence definition. The Axiom of Choice.

[F1]

The full conditional event identity is $π (C \cap p_{- B}^{- 1} (D)) = \int_{D} K_{B} (z, C_{z}) π_{- B} (d z)$ for product-measurable $C$ and measurable $D$ . Proper full conditional kernel.

[F2]

A block update retains $Z$ and draws the new block from $K_{B} (Z, \cdot)$ . Exact Gibbs block update.

[F3]

Conditional independence means $E [f (U) g (V) ∣ σ (Z)] = E [f (U) ∣ σ (Z)] E [g (V) ∣ σ (Z)]$ almost surely for all bounded measurable real $f, g$ . Conditional independence given a sigma-algebra.

[F4]

Two probability kernels with common source have a probability-kernel product whose rectangle evaluations are the products of the two evaluations. Finite products of probability kernels are probability kernels.

[F5]

A probability measure and probability kernel define a joint probability law by integrating the kernel over the first marginal, with the corresponding iterated-integral identity. A prior and model kernel define a joint law.

[F6]

Integrating a bounded measurable function against a probability kernel gives a measurable function of the source. Measurability of integration against a kernel.

[F7]

Finite measures agreeing on the generating rectangles agree on the product sigma-algebra. Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system.

Proof

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

1.1F1F2F4F5F7construct

Set $D = S_{- B}$ in [F1]. This identifies the law of $(Z, U)$ with $π_{- B} (d z) K_{B} (z, d u)$ on every product-measurable event. By [F2], after the current $(Z, U) = (z, u)$ the refreshed block $V$ has law $K_{B} (z, \cdot)$ . Form the product probability kernel $K_{B} (z, \cdot) \otimes K_{B} (z, \cdot)$ using [F4] and mix it against $π_{- B}$ by [F5]. For a rectangle $D \times A \times C$ , the first conditional identity gives probability $K_{B} (z, A)$ for $U \in A$ at retained value $z$ , and the update gives probability $K_{B} (z, C)$ for $V \in C$ ; iterating yields $\int_{D} K_{B} (z, A) K_{B} (z, C) π_{- B} (d z)$ . This is also the rectangle value of the constructed triple law. Both are probability measures, so [F7] makes them equal on the product sigma-algebra.

2.1F1F3step 1.1

For measurable $A, C \subseteq S_{B}$ and $D \in S_{- B}$ , the triple-law formula from step 1.1 gives $P (Z \in D, U \in A, V \in C) = \int_{D} K_{B} (z, A) K_{B} (z, C) π_{- B} (d z)$ . The same formula with one of $A, C$ equal to the whole block space gives the two marginal testing identities. Hence, by testing on every event ${Z \in D}$ , $K_{B} (Z, A)$ and $K_{B} (Z, C)$ are versions of the corresponding conditional expectations, and their product is a version of the conditional expectation of $1_{A} (U) 1_{C} (V)$ . The conditional-independence identity [F3] therefore holds for indicator functions.

3.1A1F3F6step 2.1algebra∎

Finite linear combinations extend the identity in step 2.1 to finite-valued measurable simple functions. For bounded measurable real $f, g$ , partition bounded intervals containing their ranges into finitely many subintervals of length below $1 / n$ and choose one value on each inverse-image set; this gives finite-valued measurable simple $f_{n}, g_{n}$ with uniform errors tending to zero. By [F6], $h_{f} (z) = \int f d K_{B} (z, \cdot)$ and $h_{g} (z) = \int g d K_{B} (z, \cdot)$ are measurable; uniform approximation also gives uniform convergence of $h_{f_{n}}$ to $h_{f}$ and $h_{g_{n}}$ to $h_{g}$ . Since the functions are uniformly bounded, the products $f_{n} (U) g_{n} (V)$ and $h_{f_{n}} (Z) h_{g_{n}} (Z)$ converge uniformly to their respective limits, so their testing identities over every ${Z \in D}$ pass to the limit. Thus $h_{f} (Z)$ and $h_{g} (Z)$ are the two conditional-expectation versions and $h_{f} (Z) h_{g} (Z)$ is a version for the product, proving [F3] for all bounded $f, g$ . AC is used only for this class-valued notation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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