Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

Continuous-time stopping times and stopped sigma-algebras

Definition

Let (Ω,F,P) be a probability space and let (Ft)t≥0 be a continuous-time filtration Continuous-time filtrations and all-pairs martingales.

  1. A map τ:Ω→[0,∞] (infinite values allowed) is a stopping time for (Ft) when {τ≤t}∈Ftfor every t≥0.
  2. For a stopping time τ its stopped sigma-algebra is Fτ:={A∈F:A∩{τ≤t}∈Ft for every t≥0}.

The following facts are used below, and each is a direct set computation.

(a) Fτ is a sigma-algebra: ∅∩{τ≤t}=∅∈Ft; for A∈Fτ one has Ac∩{τ≤t}={τ≤t}∖(A∩{τ≤t})∈Ft; and for a sequence An∈Fτ the union satisfies (⋃nAn)∩{τ≤t}=⋃n(An∩{τ≤t})∈Ft. All operations are literal, not modulo null sets, and no completeness of the filtration is assumed. (b) If τ≡t0<∞ is deterministic, then A∩{τ≤t} is A for t≥t0 and ∅ for t<t0, so Fτ=⋂t≥t0Ft=Ft0, where the last equality follows because the intersection includes its least member Ft0. If τ≡∞, then every test event {τ≤t} is empty and Fτ=F. (c) Suppose the filtration is right-continuous. Then τ is a stopping time if and only if {τ<t}∈Ft for every t>0. Indeed {τ<t}=⋃n≥1{τ≤t−1n} (with the terms for t−1n<0 read as the empty set, since τ≥0), which gives the forward implication; conversely {τ≤t}=⋂n≥1{τ<t+1n}, and ⋂nFt+1/n=⋂s>tFs=Ft by right-continuity together with monotonicity of the filtration. (d) Under the same right-continuity assumption, for A∈F one has A∈Fτ if and only if A∩{τ<t}∈Ft for every t>0: the forward implication follows from A∩{τ<t}=⋃n(A∩{τ≤t−1n}) and the converse from A∩{τ≤t}=⋂n(A∩{τ<t+1n}) together with ⋂nFt+1/n=Ft.

Because the two versions of each test are interchangeable exactly when the filtration is right-continuous, the convention is recorded here once: the Brownian strong Markov theorem is stated for the usual augmentation, which is right-continuous, and the raw-filtration statements use the non-strict test directly. No choice principle is used by this definition.

Source notes

Durrett, Section 7.3, and Sousi, Section 6.4, define stopping times by {τ≤t}∈Ft and record the strict-test form for right-continuous filtrations. The stopped sigma-algebra convention is fixed here because the strong Markov theorem and the dyadic ceiling argument both consume the containment Fτ⊆Fτn for τn↓τ.

Depends on

Used by

Dependency tree · two levels

6 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