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.
General semimartingale calculus is outside this block
Remark
The stochastic-integration and Ito-formula part of this page is scoped to continuous Brownian-driven Ito processes: processes of the form Continuous Brownian Ito processes, their quadratic covariation along deterministic partition sequences Quadratic covariation of Brownian Ito processes Quadratic variation along a partition sequence, and the one- and multidimensional Ito formula items One-dimensional Ito formula Multidimensional Ito formula for Brownian-driven processes.
The partition definitions are broader. The pathwise quadratic-variation definition takes an arbitrary continuous real function and a specified partition sequence. The process covariation definition takes arbitrary real processes with measurable fixed-time values and almost-sure continuous paths; it imposes no Brownian representation, filtration or adaptedness. It names a covariation only when its stated common uniform-in-probability limit exists. These definitions do not assert existence for every continuous process. The page also contains characterizations stated for continuous local martingales; such statements do not construct integration against every such martingale.
Outside the block. The following are not defined, proved or used here, and none of the statements on this page may be quoted as covering them:
- Ito formulas with jump terms and integration with respect to discontinuous semimartingales or compensated random measures;
- stochastic integration against a general continuous local martingale or a general semimartingale, and a general existence theory of covariation for those integrators; the Brownian integral of this block is not a general stochastic integral;
- the Burkholder--Davis--Gundy inequalities and the predictable quadratic variation , which are distinct from the realized partition-limit objects used here;
- change of measure (Girsanov theory) and exponential tilting beyond the explicit exponential Brownian martingale;
- existence and uniqueness theory for stochastic differential equations;
- Tanaka's formula, local time, and reflection-type decompositions;
- stochastic differential geometry, stochastic flows and manifold-valued diffusions.
Boundary of the covariation definition. The symbol used on this page is defined by limits along deterministic partition sequences with mesh tending to zero, and only when one common limit arises for every such sequence Quadratic covariation of Brownian Ito processes. Results stated for that convention do not automatically transfer to random, path-adapted or non-vanishing-mesh partitions, and no such transfer is claimed.
This remark records intended scope and the domains of the cited definitions. It does not prove the formula items or enlarge their hypotheses. No choices are made here; the cited stochastic constructions retain their declared AC assumptions.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
50 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, Martingales, Diffusions and Financial Mathematics (preliminary notes), Sections 5.8-5.9 (standard reference, not scraped)