Alphabeta Math
Pipeline-generated
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.

✓ 2 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Forward Itô SDE Well-Posedness — Examples

1 · Prerequisites

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

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A scalar Ornstein–Uhlenbeck SDE satisfies the strong well-posedness hypotheses

Example

Fix T>0, θ≥0, and σ0∈R∖{0}. On a complete usual filtered probability space, let W be a filtration-relative standard scalar Brownian motion and let X0 be F0-measurable, square-integrable, and independent of the future Brownian increments. Consider dXt=−θXt dt+σ0 dWt,0≤t≤T. In dimension one, a constant diffusion is nondegenerate when its variance σ02 is positive.

Facts & Assumptions

Given: The data above, the coefficient maps b(t,x)=−θx and σ(t,x)=σ0, and the Itô SDE conventions of the A page.

[F1]

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 F0 initial value in L2. Itô SDE data and strong solution

[F2]

Under those hypotheses the SDE has an adapted continuous strong solution, unique up to indistinguishability, with finite Esup⁡t≤T∣Xt∣2. Global strong well-posedness for Lipschitz Itô SDEs

Verification

1.1givenF1algebra

The coefficients are jointly Borel. For all x,y, ∣b(t,x)−b(t,y)∣+∣σ(t,x)−σ(t,y)∣=θ∣x−y∣, so the uniform Lipschitz constant can be L=θ. Also ∣b(t,x)∣+∣σ(t,x)∣=θ∣x∣+∣σ0∣≤(θ+∣σ0∣)(1+∣x∣), so the linear-growth constant can be K=θ+∣σ0∣. Finally σ02>0, so the constant scalar diffusion is nondegenerate.

2.1givenF1F2step 1.1∎

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 [0,T] and its finite path-sup second moment.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A deterministic initial law is singular although the SDE is well-posed

Example

Assume Full AC. Fix T>0 and use a complete usual filtered probability space carrying a filtration-relative standard scalar Brownian motion W. Set X0=0, b(t,x)=0, and σ(t,x)=1, so dXt=dWt,0≤t≤T. The initial law is the point mass at 0. It is concentrated on a Lebesgue-null set, although the strong well-posedness theorem applies. A Lebesgue density for a probability law μ on R means a nonnegative Lebesgue-measurable function g such that μ(A)=∫Ag dλ for every Borel set A, 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.

[F1]

The SDE definition requires jointly Borel coefficients, uniform global state Lipschitz and linear-growth bounds, and an F0-measurable L2 initial value independent of future Brownian increments. Itô SDE data and strong solution

[F2]

Under those hypotheses, there is a unique adapted continuous strong solution on the given space. Global strong well-posedness for Lipschitz Itô SDEs

[F3]

The law of a random element X0 assigns a measurable target set A the probability P(X0∈A). Law or distribution of a random element

[F4]

Lebesgue outer measure is the infimum of the sums of μ0 over countable elementary covers. Every half-open box is elementary and has μ0(B)=vol⁡(B); in dimension one, (−1/n,1/n] is a half-open interval of volume 2/n. Lebesgue outer measure on Rn Elementary sets: the finite unions of half-open boxes in Rn The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition Half-open boxes in Rn and their volume

[F6]

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

[F7]

The singleton {0} is Borel: for each x≠0, ∣x∣/2>0, and if y∈N∣x∣/2(x) then ∣x∣≤∣x−y∣+∣y∣<∣x∣/2+∣y∣, so y≠0. Thus R∖{0} is open and {0} is closed; closed sets are Borel. The ε-neighbourhood and the punctured ε-neighbourhood of a point of R Basic properties of the absolute value The triangle inequality Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen The Borel sigma-algebra of a topological space

[F8]

For any real a≥0 with a≤2/n for every n≥1, one has a=0: if a>0, the Archimedean property supplies n>2/a, so 2/n<a, a contradiction. Every complete ordered field is Archimedean

Verification

1.1F1F2given

The maps b(t,x)=0 and σ(t,x)=1 are jointly Borel. Their state Lipschitz constant is L=0, and ∣b(t,x)∣+∣σ(t,x)∣=1≤1(1+∣x∣) gives K=1. The constant diffusion is nondegenerate because its scalar variance is 1. The deterministic X0=0 is F0-measurable, square-integrable, and independent of the Brownian increments, so [F1] holds; applying [F2] gives strong well-posedness.

1.2F3F4F7F8given

By [F3] and [F7], the initial law μ satisfies μ({0})=P(X0=0)=1. For every n≥1, the half-open interval (−1/n,1/n] covers {0} and is an elementary set of volume 2/n; by [F4] its outer-measure cover cost is 2/n. Hence 0≤λ∗({0})≤2/n for every n, so λ∗({0})≤2 is finite. If λ∗({0})>0, [F8] supplies n>2/λ∗({0}), contradicting the bound; therefore λ∗({0})=0.

2.1F3F5F6F7step 1.2given∎

By [F5], {0} is Lebesgue measurable and λ({0})=0. If a Lebesgue density g for μ existed, [F6] would give μ({0})=∫{0}g dλ=0: every nonnegative simple minorant of g1{0} 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 t=0; no claim about positive-time densities is made.

Sources