TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

Doob-Dynkin factorization through the sigma-algebra generated by a function

Statement

Let $f : X \to R$ and $g : X \to \overline{R}$ . Then $g$ is $σ (f)$ -measurable if and only if there is a Borel measurable function $h : R \to \overline{R}$ such that

$g = h \circ f .$

Facts & Assumptions

Given: Functions $f : X \to R$ and $g : X \to \overline{R}$ .

[L1]

The sigma-algebra generated by $f$ is $σ (f) = {f^{- 1} (B) : B \in B (R)}$ . (The sigma-algebra generated by a function)

[L2]

Threshold measurability characterizes $\overline{R}$ -valued measurability. (Threshold characterisations of real-valued and extended-real-valued measurability)

Proof

technique · direct

1.1

If $g = h \circ f$ for a Borel measurable $h$ , then for every Borel set [L1] $B \subseteq \overline{R}$ ,

$(h \circ f)^{- 1} (B) = f^{- 1} (h^{- 1} (B)) \in σ (f),$

because $h^{- 1} (B)$ is Borel in $R$ and [L1] describes exactly the sets whose preimages under $f$ lie in $σ (f)$ . So $g$ is $σ (f)$ -measurable. [L1]

2.1

Conversely, assume $g$ is $σ (f)$ -measurable. For each rational [step 1.1, L1, L2, algebra] $q \in Q$ , the threshold set ${g \leq q}$ lies in $σ (f)$ by [L2], so [L1] provides a Borel set $A_{q} \subseteq R$ with

${g \leq q} = f^{- 1} (A_{q}) .$

Define

$B_{q} : = ⋂_{\begin{array}{c} r \in Q \\ r > q \end{array}} A_{r} .$

Then each $B_{q}$ is Borel, the family $(B_{q})_{q \in Q}$ is increasing in $q$ , and

${g \leq q} = f^{- 1} (B_{q})$

for every rational $q$ , because ${g \leq q} = ⋂_{r > q, r \in Q} {g \leq r}$ . [L1, L2, algebra]

3.1

For $y \in R$ , define

step 2.1L2

$h (y) : = \inf {q \in Q : y \in B_{q}},$

with the infimum taken in $\overline{R}$ , so the empty-set case gives $+ \infty$ . Because the sets $B_{q}$ are increasing,

${y : h (y) \leq q} = B_{q} (q \in Q),$

so [L2] makes $h$ Borel measurable. [step 2.1, L2]

4.1

Fix $x \in X$ and write $t : = g (x)$ . If $q < t$ is rational, then [step 2.1, step 3.1, L2] $x \notin {g \leq q} = f^{- 1} (B_{q})$ , so $f (x) \notin B_{q}$ and therefore $h (f (x)) > q$ . If $q \geq t$ is rational, then $x \in {g \leq q} = f^{- 1} (B_{q})$ , so $f (x) \in B_{q}$ and therefore $h (f (x)) \leq q$ . Thus $h (f (x))$ is at once at least every rational below $t$ and at most every rational above $t$ , which forces $h (f (x)) = t = g (x)$ .

step 2.1step 3.1L2

5.1

Steps 1.1 and 4.1 prove the two directions of the equivalence.

step 1.1step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Mathematics@CUHK, Martingale Theory I, Section 2.6 (standard reference, not scraped)