Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Optional stopping under uniform integrability

Statement

Assume AC. Let M be a uniformly integrable martingale and let στ be pointwise ordered, almost-surely finite stopping times. Define Mσ and Mτ using the fixed cemetery value 0 on the respective null events where the stopping time is infinite. Then Mσ,MτL1 and E[MτFσ]=Mσa.s.,EMτ=EMσ.

Facts & Assumptions

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

[F1]

Closed martingale characterization supplies ML1 with Mn=E[MFn] and makes conditional expectations of this fixed variable uniformly integrable.

[F2]

Optional sampling for bounded stopping times handles every truncated time.

[F3]

Stopped random variable and stopped process gives pointwise stabilization at an almost-surely finite time.

[F4]

Sigma-algebra at a stopping time gives the stopped-event tests, and Tower property of conditional expectation applies to nested sigma-algebras.

[F5]

The Axiom of Choice records the background AC hypothesis. The conditional-expectation and representative properties used here are supplied by [F1], [F2], and [F4].

[F6]

The stopping-time sigma-algebra is a sigma-algebra proves FσFτ for pointwise στ.

Proof

1.1

Fix a stopping time ρ equal to either σ or τ. For rn, F2 applied to ρnr gives Mρn=E[MrFρn]. Let r in L1 using F1 and conditional contraction to obtain Mρn=E[MFρn].

F1F2
2.1

The sigma-algebras Fρn increase with n. Thus the sequence in step 1.1 is a closed, hence uniformly integrable, martingale by F1. Since ρ< almost surely, F3 gives MρnMρ almost surely; F1's UI convergence implication upgrades this to L1, proving MρL1.

F1F3step 1.1
3.1

For AFρ, the event A{ρn} belongs to Fρn (check the defining finite-level intersections). Apply the conditional identity in step 1.1 on this event, then let n. The left side converges by step 2.1; the right side converges by dominated convergence for M1A{ρn}. Hence AMρdP=AMdP, so Mρ=E[MFρ].

F1F4step 1.1step 2.1
4.1

Since στ pointwise, F6 gives FσFτ. Apply the tower property in F4 to the two representations from step 3.1: E[MτFσ]=E[E[MFτ]Fσ]=E[MFσ]=Mσ. Taking expectations finishes. AC is the background hypothesis recorded in F5; the conditional-expectation identities come from F1 and F4.

F1F4F5F6step 3.1

Depends on

Used by

Dependency tree · two levels

21 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