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.
Forward Itô SDE Well-Posedness — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Brownian Motion Construction and Continuity
- Brownian Motion, Markov Properties and Hitting Times
- Brownian Path Properties
- Central Limit Theorems
- Characteristic Functions Inversion and Continuity
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Conditional Distributions and Regular Conditional Probability
- Conditional Expectation
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convexity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Cyclic Groups and Direct Products
- Darboux, L'Hôpital, and Taylor's Theorem
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Discrete Time Martingales
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Forward Itô SDE Well-Posedness
- Foundations of the Real Numbers for Analysis
- Fourier Transform Convolution and Approximate Identities
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hausdorff via the Diagonal
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Independence Borel Cantelli and Zero One Laws
- Infinite Product Measures and Kolmogorov Extension
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Itos Formula and Brownian Martingales
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Martingale Inequalities and Convergence
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Modes of Convergence for Random Variables
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Probability Spaces Random Variables and Expectation
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Splitting Fields
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Inverse and Implicit Function Theorems
- The Ito Integral with Respect to Brownian Motion
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Urysohn's Lemma and the Tietze Extension Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Convergence Tightness and Representation
2 · Summary
The examples check a scalar linear drift with nondegenerate constant diffusion against every strong-solution hypothesis, then use a deterministic initial value to show the limit of that conclusion: strong well-posedness permits an initial law concentrated on a Lebesgue-null singleton and does not itself assert a density at the initial endpoint.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A scalar Ornstein–Uhlenbeck SDE satisfies the strong well-posedness hypotheses
Example
Fix , , and . On a complete usual filtered probability space, let be a filtration-relative standard scalar Brownian motion and let be -measurable, square-integrable, and independent of the future Brownian increments. Consider In dimension one, a constant diffusion is nondegenerate when its variance is positive.
Facts & Assumptions
Given: The data above, the coefficient maps and , and the Itô SDE conventions of the A page.
The global well-posedness contract requires jointly Borel coefficients, uniform global state Lipschitz and linear-growth bounds, a filtration-relative Brownian motion, and an independent initial value in . Itô SDE data and strong solution
Under those hypotheses the SDE has an adapted continuous strong solution, unique up to indistinguishability, with finite . Global strong well-posedness for Lipschitz Itô SDEs
Verification
The coefficients are jointly Borel. For all , , so the uniform Lipschitz constant can be . Also , so the linear-growth constant can be . Finally , so the constant scalar diffusion is nondegenerate.
The initial value and Brownian motion satisfy the filtration and moment assumptions by the example's hypotheses. Step 1.1 verifies both coefficient bounds, so [F2] gives a unique adapted continuous strong solution on and its finite path-sup second moment.
A deterministic initial law is singular although the SDE is well-posed
Example
Assume Full AC. Fix and use a complete usual filtered probability space carrying a filtration-relative standard scalar Brownian motion . Set , , and , so The initial law is the point mass at . It is concentrated on a Lebesgue-null set, although the strong well-posedness theorem applies. A Lebesgue density for a probability law on means a nonnegative Lebesgue-measurable function such that for every Borel set , where is one-dimensional Lebesgue measure.
Facts & Assumptions
Given: the data above, the Itô SDE convention of Itô SDE data and strong solution, and Full AC.
The SDE definition requires jointly Borel coefficients, uniform global state Lipschitz and linear-growth bounds, and an -measurable initial value independent of future Brownian increments. Itô SDE data and strong solution
Under those hypotheses, there is a unique adapted continuous strong solution on the given space. Global strong well-posedness for Lipschitz Itô SDEs
The law of a random element assigns a measurable target set the probability . Law or distribution of a random element
Lebesgue outer measure is the infimum of the sums of over countable elementary covers. Every half-open box is elementary and has ; in dimension one, is a half-open interval of volume . Lebesgue outer measure on Elementary sets: the finite unions of half-open boxes in The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition Half-open boxes in and their volume
Full AC supplies countable choice. Under countable choice, a set of Lebesgue outer measure zero is Lebesgue measurable and has Lebesgue measure zero. The Axiom of Choice AC supplies countable selections and prescribed serial paths The Axiom of Countable Choice () Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume Lebesgue measurable sets, the family , and the restricted set function
The integral over a measurable set is the nonnegative Lebesgue integral of the function times its indicator; that integral is the supremum of nonnegative simple minorants, and a simple integral is the sum of its values times the measures of their level sets. Integral over a measurable subset The nonnegative Lebesgue integral The integral of a nonnegative simple function
The singleton is Borel: for each , , and if then , so . Thus is open and is closed; closed sets are Borel. The -neighbourhood and the punctured -neighbourhood of a point of Basic properties of the absolute value The triangle inequality Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen The Borel sigma-algebra of a topological space
For any real with for every , one has : if , the Archimedean property supplies , so , a contradiction. Every complete ordered field is Archimedean
Verification
The maps and are jointly Borel. Their state Lipschitz constant is , and gives . The constant diffusion is nondegenerate because its scalar variance is . The deterministic is -measurable, square-integrable, and independent of the Brownian increments, so [F1] holds; applying [F2] gives strong well-posedness.
By [F3] and [F7], the initial law satisfies . For every , the half-open interval covers and is an elementary set of volume ; by [F4] its outer-measure cover cost is . Hence for every , so is finite. If , [F8] supplies , contradicting the bound; therefore .
By [F5], is Lebesgue measurable and . If a Lebesgue density for existed, [F6] would give : every nonnegative simple minorant of has integral zero because each positive level set is contained in the null singleton and the zero level contributes zero, so the supremum of their integrals is zero. This contradicts step 1.2. Thus the initial law has no Lebesgue density at ; no claim about positive-time densities is made.