LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Borel product probabilities on compact metric spaces by sections

Statement

Let $X, Y$ be nonempty compact metric spaces, let $μ, ν$ be countably additive Borel probability measures on $X, Y$ , and give $X \times Y$ its product topology. For every Borel set $E \subseteq X \times Y$ , its section $E_{x} : = {y \in Y : (x, y) \in E}$ is Borel in $Y$ , and $x \mapsto ν (E_{x})$ is Borel measurable. The formula $λ (E) : = \int_{X} ν (E_{x}) d μ (x)$ defines a Borel probability measure on $X \times Y$ satisfying $λ (A \times B) = μ (A) ν (B)$ for every Borel $A \subseteq X$ and $B \subseteq Y$ . In particular its coordinate marginals are $μ, ν$ .

Facts & Assumptions

Given: The compact metric spaces, probabilities, and product topology in the Statement.

[F1]

Distance to a nonempty set is 1-Lipschitz. A closed subset of a compact metric space is compact. $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz A closed subset of a compact metric space is compact

[F2]

If an open set in $Y \times X$ contains $K \times {x}$ for compact $K \subseteq Y$ , the tube lemma gives an open neighborhood $V$ of $x$ with $K \times V$ contained in that set. It uses an indexed family of all admissible pairs of neighborhoods and one finite subcover, without choice. Tube lemma: if $K$ is a compact subset of a metric space $X$ , $Z$ is a topological space and $N$ is open in $X \times Z$ with $K \times {z_{0}} \subseteq N$ , then $K \times W \subseteq N$ for some open $W ∋ z_{0}$

[F3]

Measures are continuous from below on increasing measurable sequences. Continuity from below for measures

[F4]

A lambda-system containing a pi-system contains its generated sigma-algebra. Dynkin's pi-lambda theorem

[F5]

Nonnegative integrals are monotone, homogeneous and finitely additive, agree with the simple integral, and preserve increasing pointwise limits. The nonnegative Lebesgue integral Monotonicity and nonnegative homogeneity of the nonnegative integral Additivity of the nonnegative Lebesgue integral The nonnegative integral agrees with the simple integral on simple functions Monotone convergence for the integral

[F6]

A Borel sigma-algebra is generated by the open sets. Continuous maps pull Borel sets back to Borel sets, and the product topology has open rectangles as a basis. The Borel sigma-algebra of a topological space The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement

[F7]

Finite sums and real scalar multiples of real Borel measurable functions are Borel measurable, as are increasing pointwise limits of nonnegative Borel functions. Closure properties of measurable functions used by the integral

[F8]

A measure takes nonnegative values and is countably additive on disjoint measurable sets. Measures on sigma-algebras

Proof

technique · direct

1.1givenF1F3F6construct

For an open set $G \subseteq Y$ with $G \neq Y$ , put $K_{n} : = {y : d (y, Y ∖ G) \geq 1 / n}$ for integers $n \geq 1$ . By [F1] these sets are closed and compact. They increase, lie in $G$ , and exhaust $G$ : if $y \in G$ , some ball $B (y, r)$ lies in $G$ , so $d (y, Y ∖ G) \geq r > 0$ and $y \in K_{n}$ for some $n$ . If $G = Y$ , use $K_{n} = Y$ . Thus [F3] gives $ν (G) = \sup_{n} ν (K_{n})$ for a specified compact exhaustion of each open $G$ , including $G = \emptyset$ .

2.1step 1.1F2F6F8choose

Let $U \subseteq X \times Y$ be open. The map $y \mapsto (x, y)$ is continuous for fixed $x$ , so each $U_{x}$ is open. Put $h_{U} (x) = ν (U_{x})$ . If $h_{U} (x) > a$ for $a \geq 0$ , step 1.1 provides one compact $K \subseteq U_{x}$ with $ν (K) > a$ . The coordinate interchange $S : Y \times X \to X \times Y$ , $S (y, z) = (z, y)$ , is a homeomorphism: it and its inverse take basic open rectangles to basic open rectangles by [F6]. Thus $S^{- 1} (U)$ is open and contains $K \times {x}$ . Apply [F2] in $Y \times X$ to obtain an open neighborhood $V$ of $x$ with $K \times V \subseteq S^{- 1} (U)$ , or equivalently $V \times K \subseteq U$ . For every $z \in V$ , $K \subseteq U_{z}$ and $h_{U} (z) = ν (U_{z})$ . The set $K$ is one of the closed sets in the exhaustion from step 1.1, and $U_{z}$ is open, so $K$ and $U_{z} ∖ K$ are Borel by [F6]. Their disjoint union is $U_{z}$ ; apply countable additivity to the disjoint sequence $K, U_{z} ∖ K, \emptyset, \dots$ [F8]. Nonnegativity of $ν$ [F8] then gives $h_{U} (z) = ν (K) + ν (U_{z} ∖ K) \geq ν (K) > a$ . Consequently ${h_{U} > a}$ is open for every real $a$ (for $a < 0$ it is all of $X$ ). Hence $h_{U}$ is lower semicontinuous and Borel: the inverse images of real rays $(a, + \infty)$ are open, and these rays generate the real Borel sigma-algebra, as their rational subfamily generates all open intervals by countable unions and complements.

3.1step 2.1F4F6F7construct

Every Borel $E \subseteq X \times Y$ has Borel sections because the continuous map $y \mapsto (x, y)$ has inverse image $E_{x}$ . Let $D$ be the family of Borel $E$ for which $h_{E} (x) : = ν (E_{x})$ is Borel. It contains $X \times Y$ , with $h = 1$ . If $E \in D$ , then $h_{E^{c}} = 1 - h_{E}$ is Borel by [F7]. For disjoint $E_{n} \in D$ , countable additivity of $ν$ gives $h_{⋃_{n} E_{n}} = \sum_{n} h_{E_{n}}$ , an increasing limit of Borel partial sums and therefore Borel by [F7]. Thus $D$ is a lambda-system. All open sets belong to it by step 2.1; the open sets form a pi-system generating $B (X \times Y)$ . By [F4], $D = B (X \times Y)$ .

4.1step 3.1F5construct

Define $λ (E) = \int h_{E} d μ$ , which is meaningful and lies in $[0, 1]$ by step 3.1 and [F5]. It has $λ (\emptyset) = 0$ and $λ (X \times Y) = 1$ . For disjoint Borel $E_{n}$ , step 3.1 gives $h_{⋃_{n} E_{n}} = \lim_{N} \sum_{n = 1}^{N} h_{E_{n}}$ increasingly. Finite additivity and monotone convergence [F5] yield $λ (⋃_{n} E_{n}) = \lim_{N} \sum_{n = 1}^{N} λ (E_{n}) = \sum_{n} λ (E_{n})$ . Hence $λ$ is a countably additive Borel probability.

5.1step 4.1F5F6∎

For Borel $A \subseteq X, B \subseteq Y$ , the rectangle $A \times B$ is Borel as the intersection of the two coordinate inverse images. Its section measure is $h_{A \times B} (x) = 1_{A} (x) ν (B)$ . The simple-integral formula [F5] gives $λ (A \times B) = μ (A) ν (B)$ . Taking $B = Y$ or $A = X$ proves the marginal identities.

Remarks

This construction works on the full Borel sigma-algebra of the product topology. It neither asserts nor uses equality with the sigma-algebra generated by Borel rectangles. It requires no simultaneous selection of finite nets. The integral convergence is over specified sequences, and the compact exhaustion in step 1.1 is given by a formula. A general optimal-coupling attainment theorem is not part of this lemma.

Depends on

Used by

A finite coupling lifts to a Borel coupling with a controlled metric cost Lemma

Dependency tree · two levels

71 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

John K. Hunter, Measure Theory, product-measure construction by measurable sections (adapted here to product-topology Borel sets) (standard reference, not scraped)