Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Conditional-independence splice lemma

Statement

Assume Choice. Let μ12 on S1×S2 and μ23 on S2×S3 be probability measures with the same S2 marginal, where all three spaces are standard Borel. There is a unique probability measure μ on S1×S2×S3 whose (1,2) and (2,3) marginals are μ12 and μ23 and under which the first and third coordinates are conditionally independent given the second.

Facts & Assumptions

Given: Choice, the three standard-Borel spaces and the compatible laws in the statement. Denote their common S2 marginal by μ2.

[F1]

A regular conditional distribution exists for a standard-Borel target. (Existence of regular conditional distributions for standard borel targets)

[F2]

Such a conditional kernel given a standard-Borel random element factors through that element as an everywhere probability kernel. (Regular conditional kernels factor through a standard borel conditioning variable)

[F3]

Integrating a nonnegative product-measurable function against a finite kernel produces a measurable function of the source variable. (Measurability of integration against a kernel)

[F4]

Monotone convergence applies to nonnegative measurable integrands. (Monotone convergence for the integral)

[F5]

Conditional independence is equivalent to invariance of the conditional law of one side when the other side is adjoined to the conditioning sigma-algebra. (Conditional-independence equivalences and preservation)

[F6]

Equality of two probability measures on a generating pi-system extends to the generated sigma-algebra. (Dynkin's pi-lambda theorem)

[F7]

Sections of product-measurable functions, in particular indicators of product-measurable sets, are measurable. (Every section of a product-measurable function is measurable)

Proof

1.1F1F2

Apply [F1] to the coordinate pair on [F1, F2] (S2×S3,μ23) and then [F2]. This gives a probability kernel Q:S2→S3 such that, for A2,A3 measurable, μ23(A2×A3)=∫A2Q(s2,A3) μ2(ds2). Choice is used precisely by [F1]--[F2] to select and factor the conditional law.

2.1F3F4F7step 1.1

Lift Q to the kernel [F3, F4, F7, step 1.1] Q~((s1,s2),⋅)=Q(s2,⋅) and, for a measurable C⊆S1×S2×S3, set μ(C)=∫S1×S2Q(s2,C(s1,s2)) μ12(d(s1,s2)). Each section C(s1,s2) is measurable by [F7], and the integrand is measurable by [F3], applied to 1C and Q~. For disjoint Cj, their sections are disjoint and [F4] passes the increasing partial sums through the outer integral. Thus μ is countably additive; μ(∅)=0 and μ(S1×S2×S3)=1. Hence it is a probability measure, including when one of the displayed test sets below is empty.

3.1F6step 1.1step 2.1

Taking C=A1×A2×S3 in step 2.1 gives [F6, step 1.1, step 2.1] μ(C)=μ12(A1×A2). Taking C=S1×A2×A3 and using step 1.1 gives μ(C)=μ23(A2×A3). The rectangle pi-systems and [F6] therefore identify both required marginals on their full product sigma-algebras.

4.1F3F5step 1.1step 2.1step 3.1

For bounded measurable g:S3→R, write [F3, F5, step 1.1, step 2.1, step 3.1] Qg(s2)=∫g(s3)Q(s2,ds3). The construction in step 2.1, first for indicators, then for simple functions, and then for positive and negative parts, shows Eμ[g(S3)∣σ(S1,S2)]=Qg(S2). The (2,3) marginal and step 1.1 likewise show Eμ[g(S3)∣σ(S2)]=Qg(S2). Criterion [F5] now gives S1⊥ ⁣ ⁣ ⁣⊥S3∣S2.

5.1F5F6step 2.1step 3.1∎

Let ν be any other law with the two marginals and the stated [F5, F6, step 2.1, step 3.1] conditional independence. Its (2,3) marginal makes Qg(S2) a conditional expectation of g(S3) given S2; [F5] then makes it the conditional expectation given (S1,S2). Consequently, for every measurable rectangle, ν(A1×A2×A3)=∫1A1(s1)1A2(s2)Q(s2,A3) dμ12, which equals the value of μ from step 2.1. Rectangles form a pi-system containing the whole space, so [F6] gives ν=μ.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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