TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

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.

For sigma-finite measures, the two section-measure integrals of a measurable set agree

Statement

Let $(X, A, μ)$ and $(Y, B, ν)$ be sigma-finite measure spaces, and let $E \in A \otimes B$ . Then

$\int_{X} ν (E_{x}) d μ = \int_{Y} μ (E^{y}) d ν .$

Facts & Assumptions

Given: Sigma-finite measure spaces $(X, A, μ)$ and $(Y, B, ν)$ , and a set $E \in A \otimes B$ .

[L1]

The section-measure functions $x \mapsto ν (E_{x})$ and $y \mapsto μ (E^{y})$ are measurable. (For sigma-finite measures, the section-measure functions are measurable)

[L2]

Finite disjoint unions of measurable rectangles form an algebra generating $A \otimes B$ . (Finite disjoint unions of measurable rectangles form an algebra generating the product sigma-algebra)

[L3]

The monotone class generated by an algebra coincides with the generated sigma-algebra. (The monotone class generated by an algebra equals the sigma-algebra it generates)

[L4]

Monotone convergence allows integrals of increasing nonnegative functions to pass to the limit. (Monotone convergence for the integral)

[A1]

Since $μ$ and $ν$ are sigma-finite, there are measurable exhaustions $X_{n} ↑ X$ and $Y_{n} ↑ Y$ with $μ (X_{n}), ν (Y_{n}) < \infty$ .

Proof

technique · direct

1.1

Fix $n, m \geq 1$ . Let $D_{n, m}$ be the family of measurable subsets $F \subseteq X_{n} \times Y_{m}$ such that $\int_{X_{n}} ν (F_{x}) d μ = \int_{Y_{m}} μ (F^{y}) d ν .$ If $F = (A \times B) \cap (X_{n} \times Y_{m})$ , then $F_{x} = (B \cap Y_{m})$ for $x \in A \cap X_{n}$ and $\emptyset$ otherwise, so both integrals equal $μ (A \cap X_{n}) ν (B \cap Y_{m})$ . Finite additivity gives the same equality for the algebra of [L2].

L2L3A1

1.2

If $F_{k} ↑ F$ inside $X_{n} \times Y_{m}$ , then [L1] and [L4] give $\int_{X_{n}} ν ((F_{k})_{x}) d μ ↑ \int_{X_{n}} ν (F_{x}) d μ,$ and similarly on $Y_{m}$ . Thus $D_{n, m}$ is a monotone class. By [L2] and [L3], every measurable subset of $X_{n} \times Y_{m}$ belongs to $D_{n, m}$ .

L1L4L2L3

2.1

Put $E_{n, m} : = E \cap (X_{n} \times Y_{m})$ . Step 1.2 gives $\int_{X_{n}} ν ((E_{n, m})_{x}) d μ = \int_{Y_{m}} μ ((E_{n, m})^{y}) d ν .$ Now $(E_{n, m})_{x} = E_{x} \cap Y_{m}$ for $x \in X_{n}$ and $\emptyset$ otherwise, so as $n, m \to \infty$ the two integrands increase pointwise to $ν (E_{x})$ and $μ (E^{y})$ .

step 1.2A1

3.1

Applying [L4] on both sides of step 2.1 and then letting $n, m \to \infty$ gives $\int_{X} ν (E_{x}) d μ = \int_{Y} μ (E^{y}) d ν .$ This is the claimed equality.

L4step 2.1L1∎

Depends on

Used by

Dependency tree · two levels

29 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

Terence Tao, An Introduction to Measure Theory, Theorem 1.7.15 (standard reference, not scraped)