CounterexampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedaudited 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.

Product-measure equality is not pointwise equality

Statement refuted

The inference "two integrands that agree $(d t \otimes P)$ -almost everywhere agree as raw processes, and their Ito integrals agree because the processes agree" is false as stated. The deterministic processes $H (t, ω) : = 1_{{t = 1 / 2}}, K (t, ω) : = 0$ are predictable with finite energy and agree $(d t \otimes P)$ -almost everywhere, but as raw processes they differ exactly on ${1 / 2} \times Ω$ : their sections at $t = 1 / 2$ differ at every $ω$ , while they agree at every $t \neq 1 / 2$ . Their Ito integrals on $[0, T]$ are nevertheless equal almost surely, so the correct equality is the almost-everywhere class, not pointwise agreement.

Facts & Assumptions

Given: AC, a horizon $T > 1 / 2$ , the deterministic processes $H = 1_{{1 / 2}}$ and $K = 0$ .

[F1]

$H$ and $K$ are predictable: a deterministic Borel function of the time variable is a predictable process, $1_{[0, 1 / 2]}$ and the pointwise limit $1_{[0, 1 / 2)} = \lim_{n \to \infty} 1_{[0, 1 / 2 - 1 / (n + 3)]}$ of predictable indicators are predictable, and $1_{{1 / 2}} = 1_{[0, 1 / 2]} - 1_{[0, 1 / 2)}$ . Progressively measurable and predictable processes

[F2]

$d t \otimes P ({1 / 2} \times Ω) = 0$ : the section at $ω$ is the singleton ${1 / 2}$ , which is Lebesgue-null, so Tonelli gives the value $0$ . Hence $H = K$ almost everywhere for the product measure, and both have finite energy, $\int_{0}^{T} ⁣ ⁣ \int H^{2} d P d t = 0$ . Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F3]

The Ito integral is a function of the $(d t \otimes P)$ -class of the integrand: if two finite-energy predictable integrands agree almost everywhere, their integrals agree almost surely. The general Ito integral is well defined Ito integral for square-integrable predictable processes

[F4]

AC is declared for the ambient interfaces. The Axiom of Choice

Counterexample

1.1

The two raw processes differ exactly on the time section ${1 / 2}$ : for $t = 1 / 2$ one has $H = 1 \neq 0 = K$ at every $ω$ , while for $t \neq 1 / 2$ both vanish; by [F2] the exceptional set has product measure zero, so the processes are equal in the $L^{2} (d t \otimes P)$ sense while failing pointwise equality for every $ω$ .

F2given

1.2

Both processes are predictable by [F1] and have finite energy: $H^{2} = H$ integrates to $0$ and $K^{2} = 0$ , so both integrals over $[0, T]$ are defined as classes.

F1F2

2.1

By [F3] the integrals agree, $\int_{0}^{T} H d B = \int_{0}^{T} K d B = 0$ almost surely, because the integrands differ on a product-null set; the equality of integrals is therefore not evidence of pointwise equality of the integrands.

F3step 1.1step 1.2

3.1

The example isolates the convention in force throughout this development: representatives of predictable $L^{2}$ classes are interchangeable, deterministic singleton sections are invisible to the product measure, and every statement about an Ito integral is a statement about an almost-everywhere class. The degenerate variant $H = 1_{{0}}$ agrees with $K = 0$ even as a raw process on $(0, T]$ , since the elementary convention makes the value at time zero irrelevant; the singleton ${1 / 2}$ exhibits the genuine pointwise failure. AC enters only through [F4].

F3step 2.1F4given∎

Source notes

Van der Vaart, Definition 5.25, defines the $L^{2}$ integral for equivalence classes of integrands; the example records that the equivalence is strictly coarser than pointwise equality, so citations to "the integrand" always mean its product-measure class.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

Aad van der Vaart, Stochastic Integration and Differential Equations, Definition 5.25 (standard reference, not scraped)