ExampleConstruction: Literature-sourcedVerification: 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.

An Lp-bounded martingale with an Lp terminal value

Statement

Assume AC. If $p > 1$ , $X \in L^{p}$ , $(F_{n})$ is a filtration, and $F_{\infty}$ is a sigma-algebra containing every $F_{n}$ , then $M_{n} = E [X ∣ F_{n}]$ is $L^{p}$ -bounded and converges almost surely and in $L^{p}$ to an $F_{\infty}$ -measurable $M_{\infty}$ . If $F_{\infty} = σ (⋃_{n} F_{n})$ , then $M_{\infty} = E [X ∣ F_{\infty}]$ .

Facts & Assumptions

Given: The hypotheses, objects, and conventions in the Statement.

[F1]

Conditional expectation process is a martingale makes $(M_{n})$ a martingale.

[F2]

Conditional lp contraction gives $∥ M_{n} ∥_{p} \leq ∥ X ∥_{p}$ .

[F3]

Lp-bounded martingale convergence gives almost-sure and $L^{p}$ convergence.

[F4]

Levy upward convergence of conditional expectations identifies the generated- $σ$ -algebra limit.

[F5]

The Axiom of Choice states AC, assumed here because F1--F4 use conditional expectations and chosen representatives.

Proof

1.1F1F2F3

F1 makes $(M_{n})$ a martingale, and F2 gives $\sup_{n} ∥ M_{n} ∥_{p} \leq ∥ X ∥_{p} < \infty$ . F3 therefore supplies $M_{\infty} \in L^{p}$ with both asserted modes of convergence. As a pointwise limit of variables measurable for $F_{\infty}$ , it has an $F_{\infty}$ -measurable version.

2.1F4F5step 1.1∎

When $F_{\infty} = σ (⋃_{n} F_{n})$ , F4 gives almost-sure and $L^{1}$ convergence of the same sequence to $E [X ∣ F_{\infty}]$ . Limits in probability are unique, so it equals the $L^{p}$ limit $M_{\infty}$ almost surely. AC is used exactly through F5.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

van der Vaart, Martingales, Diffusions and Financial Mathematics, Theorems 2.23–2.25, pp. 15–16 (standard reference, not scraped)