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.

Stopping a likelihood-ratio martingale

Statement

Assume AC. Let $N \in N_{0}$ , let $(F_{n})_{0 \leq n \leq N}$ be a filtration on a probability space $(Ω, F_{N}, P)$ , and let $Q$ be a probability measure on $F_{N}$ with $Q ≪ P$ . Let $L_{n} = E_{P} [d Q / d P ∣ F_{n}], 0 \leq n \leq N .$ For every stopping time $τ \leq N$ , $L_{τ}$ is nonnegative, $F_{τ}$ -measurable, and $E_{P} L_{τ} = 1$ . Moreover $Q (A) = E_{P} [1_{A} L_{τ}] (A \in F_{τ}) .$

Facts & Assumptions

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

[F1]

A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density supplies the nonnegative terminal density $L_{N} = d Q / d P$ with mean one.

[F2]

Conditional expectation process is a martingale makes $L_{n}$ a nonnegative martingale.

[F3]

Optional sampling for bounded stopping times gives conditional and unconditional identities at $τ$ .

[F4]

A stopped random variable is measurable at the stopping time gives $F_{τ}$ -measurability.

[F5]

The Axiom of Choice is used exactly for Radon–Nikodym and conditional-expectation existence.

Proof

1.1

F1 and conditional positivity make every $L_{n}$ nonnegative; F2 makes the process a martingale. F4 makes $L_{τ}$ $F_{τ}$ -measurable. Applying F3 between $τ$ and deterministic $N$ gives $L_{τ} = E_{P} [L_{N} ∣ F_{τ}], E_{P} L_{τ} = E_{P} L_{N} = Q (Ω) = 1.$

F1F2F3F4

2.1

For $A \in F_{τ}$ , the defining conditional-expectation identity in step 1.1 gives $E_{P} [1_{A} L_{τ}] = E_{P} [1_{A} L_{N}] = Q (A),$ where the final equality is the Radon–Nikodym identity and $A \in F_{τ} \subseteq F_{N}$ . AC has precisely the role in F5.

F1F3F5step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Durrett, Probability: Theory and Examples, 5th ed., likelihood-ratio martingales in Chapter 4 (standard reference, not scraped)