LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Bounded stopping preserves càdlàg square-integrable martingales

Statement

Let $M = (M_{t})_{0 \leq t \leq T}$ be a square-integrable all-pairs martingale with right-continuous paths with left limits for every $ω$ , and let $τ \leq T$ be a stopping time. Then the stopped process $M_{t}^{τ} : = M_{t \land τ}$ is a square-integrable martingale on $[0, T]$ .

Facts & Assumptions

Given: A finite horizon, a square-integrable all-pairs martingale with pathwise càdlàg paths, and a bounded stopping time $τ$ .

[F1]

On $[0, T]$ , use the adaptedness, all-pairs conditional-expectation identity and pointwise $L^{2}$ conditions of Continuous-time adapted processes and martingales with times restricted to this interval. This agrees with its $[0, \infty)$ convention: extend $M$ and the filtration by ${\tilde{M}}_{t} = M_{t \land T}$ and ${\tilde{F}}_{t} = F_{t \land T}$ . For $s \leq T < t$ the extended martingale identity is $E [M_{T} ∣ F_{s}] = M_{s}$ ; for $T \leq s \leq t$ it is the known-variable identity, and for $s \leq t \leq T$ it is the given identity. Thus this extension is a square-integrable martingale, without any filtration augmentation.

[F2]

A map $τ$ is a stopping time when ${τ \leq t} \in F_{t}$ . (Continuous-time stopping times and stopped sigma-algebras)

[F3]

The absolute value of a martingale is a nonnegative submartingale, and the finite discrete-time Doob $L^{2}$ inequality bounds its grid maximum by twice the terminal $L^{2}$ norm. (Absolute value and powers of a martingale are submartingales Doob Lp maximal inequality)

[F4]

Dominated convergence passes limits through event integrals. (Dominated convergence)

[F5]

Increasing nonnegative integrals converge to the integral of the limit. (Monotone convergence for the integral)

[A1]

AC is inherited through the conditional-expectation interface in [F1]. (The Axiom of Choice)

Proof

1.1A1F1F3F5given

Let $π_{n}$ be nested finite partitions of $[0, T]$ containing any fixed $s, t$ with mesh tending to zero. For each $π_{n}$ , the values of $∣ M ∣$ on its grid form a discrete-time nonnegative submartingale by [F1, F3]. The Doob bound gives $E \max_{u \in π_{n}} ∣ M_{u} ∣^{2} \leq 4 E ∣ M_{T} ∣^{2}$ . Càdlàg paths and the nested dense grids imply $\sup_{u \leq T} ∣ M_{u} ∣ = \sup_{u \in \cup_{n} π_{n}} ∣ M_{u} ∣$ ; [F5] then gives $E \sup_{u \leq T} ∣ M_{u} ∣^{2} < \infty$ .

1.2A1F1F2givenalgebra

For a finite partition $π_{n} = {r_{0} < \dots < r_{m}}$ , round $τ$ up to the first grid point $τ_{n} \geq τ$ . This is a finite-valued stopping time because ${τ_{n} \leq r_{j}} = {τ \leq r_{j}} \in F_{r_{j}}$ . At adjacent grid points, $M_{r_{k} \land τ_{n}} - M_{r_{k - 1} \land τ_{n}} = 1_{{τ_{n} > r_{k - 1}}} (M_{r_{k}} - M_{r_{k - 1}})$ ; the indicator is $F_{r_{k - 1}}$ -measurable. Conditioning each increment on its left endpoint proves the stopped grid values have the martingale identity at grid times, in particular at $s, t$ .

2.1A1F1F4step 1.1step 1.2∎

Refine the partitions while keeping $s, t$ as grid points. Then $τ_{n} ↓ τ$ , and pathwise right continuity gives $M_{s \land τ_{n}} \to M_{s \land τ}$ and $M_{t \land τ_{n}} \to M_{t \land τ}$ . For $u = s$ or $u = t$ , the events ${τ_{n} = r_{j}}$ with grid value $r_{j} < u$ lie in $F_{r_{j}} \subseteq F_{u}$ , and their complement ${τ_{n} \geq u}$ is also in $F_{u}$ ; expressing $M_{u \land τ_{n}}$ over these finitely many events proves $F_{u}$ -measurability. The pointwise limits are then measurable there without completing the filtration. Both are dominated by $\sup_{u \leq T} ∣ M_{u} ∣$ , integrable by step 1.1. For each $B \in F_{s}$ , apply [F4] to the event-integral martingale identity from step 1.2; it yields $E [1_{B} (M_{t \land τ} - M_{s \land τ})] = 0$ , hence the stopped process satisfies the all-pairs martingale identity. Also $∣ M_{t \land τ} ∣ \leq \sup_{u \leq T} ∣ M_{u} ∣$ gives square integrability.

Source notes

Bass discusses martingale jump decompositions and stopped martingales. The finite-grid approximation above gives the bounded-stopping argument under this library's uncompleted filtration convention without assuming the usual conditions on the filtration.

Depends on

Used by

Brackets of a compensated simple counting process Theorem

Dependency tree · two levels

43 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

Richard F. Bass, SDEs with Jumps, Section 2.3, PDF pp. 3–4 (standard reference, not scraped)