LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

CIR Lamperti equation and unique positive implicit root

Statement

Let $κ, θ, σ > 0$ satisfy the Feller condition $2 κ θ \geq σ^{2}$ , and put $a = \frac{4 κ θ - σ^{2}}{8} .$ For a positive local strong solution of the CIR SDE $d X_{t} = κ (θ - X_{t}) d t + σ \sqrt{X_{t}} d W_{t}$ on $U = (0, \infty)$ , the Lamperti variable $Z_{t} = \sqrt{X_{t}}$ satisfies $d Z_{t} = (\frac{a}{Z_{t}} - \frac{κ}{2} Z_{t}) d t + \frac{σ}{2} d W_{t}$ up to every compact exit time. Moreover, for every $h > 0$ , $z \geq 0$ , and $Δ W \in R$ , the drift-implicit step $z_{+} = z + h (\frac{a}{z_{+}} - \frac{κ}{2} z_{+}) + \frac{σ}{2} Δ W$ has exactly one positive root. It is the value defined by Positive Lamperti drift-implicit scheme for the CIR process. The boundary input $z = 0$ is included for the numerical root statement; the CIR solution theorem below uses $X_{0} > 0$ .

Facts & Assumptions

Given: AC; positive parameters satisfying the Feller condition; a positive local CIR solution; and a positive step $h$ .

[F1]

For a continuous Brownian Itô process $X$ and $f \in C^{1, 2}$ , Itô's formula has drift $f^{'} b + \frac{1}{2} f^{''} σ^{2}$ and diffusion $f^{'} σ$ . Multidimensional Ito formula for Brownian-driven processes

[F2]

The numerical root procedure sets $A = 1 + κ h / 2$ , $c = z + σ Δ W / 2$ , and returns $(c + \sqrt{c^{2} + 4 A a h}) / (2 A)$ . Positive Lamperti drift-implicit scheme for the CIR process

[F3]

Every nonnegative real number has a unique nonnegative square root, and squaring is strictly increasing on nonnegative reals. Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$

[F4]

On $(0, \infty)$ , $(x^{1 / 2})^{'} = \frac{1}{2} x^{- 1 / 2}$ and $(x^{1 / 2})^{''} = - \frac{1}{4} x^{- 3 / 2}$ . Continuity and derivatives of positive-base real powers

[F5]

For $0 < ε < R$ , a $C^{2}$ function $g$ on $(0, \infty)$ has a global $C^{2}$ extension agreeing with it on $[ε, R]$ : choose a smooth cutoff $χ$ with support in $[ε / 2, 2 R] \subset (0, \infty)$ and equal to $1$ on $[ε, R]$ , and set $\tilde{g} = χ g$ on $(0, \infty)$ and $0$ on $(- \infty, 0]$ . Such a cutoff is given by $χ (x) = η ((x - ε / 2) / (ε / 2)) η ((2 R - x) / R)$ , where $ρ (u) = e^{- 1 / u}$ for $u > 0$ , $ρ (u) = 0$ for $u \leq 0$ , and $η (u) = ρ (u) / (ρ (u) + ρ (1 - u))$ . The stopped state remains in $[ε, R]$ , so the global Itô formula for $\tilde{g}$ uses exactly $g, g^{'}, g^{''}$ there.

[A1]

AC is inherited from the local Brownian and Itô interfaces; no additional choice is used. The Axiom of Choice

Proof

Given: The hypotheses and facts in the Statement and Facts.

1.1F1F4F5givenalgebra

For each $n$ let $D_{n} = {1 / n < X_{0} < n} \in F_{0}$ , and let $τ_{n}$ be the first exit from $[1 / n, n]$ . The events $D_{n}$ increase to a probability-one event because $X_{0} > 0$ is finite. Use [F5] to extend $f (x) = \sqrt{x}$ from that interval to a global $C^{2}$ function equal to zero off its positive support, then apply [F1] to the stopped process $X^{τ_{n}}$ . On $D_{n}$ its state stays in $[1 / n, n]$ , so the extended function and its derivatives agree with $f$ , $f^{'} (x) = 1 / (2 \sqrt{x})$ and $f^{''} (x) = - 1 / (4 x^{3 / 2})$ by [F4]. The resulting drift is $\frac{κ (θ - X_{t})}{2 \sqrt{X_{t}}} - \frac{σ^{2} X_{t}}{8 X_{t}^{3 / 2}} = \frac{4 κ θ - σ^{2}}{8 Z_{t}} - \frac{κ}{2} Z_{t} = \frac{a}{Z_{t}} - \frac{κ}{2} Z_{t}$ and the diffusion is $σ / 2$ . The countable compact exhaustion proves the identity up to every compact exit and hence on the local solution's lifetime.

1.2givenalgebra

The Feller inequality implies $4 κ θ - σ^{2} \geq σ^{2} > 0$ , so $a > 0$ . Thus for the numerical step $A = 1 + κ h / 2 > 0$ and $4 A a h > 0$ .

2.1F2F3step 1.2algebra

Multiplying the drift-implicit equation by $z_{+}$ and collecting terms gives $A z_{+}^{2} - c z_{+} - a h = 0$ , with $c = z + σ Δ W / 2$ . Its discriminant is $c^{2} + 4 A a h > c^{2}$ , so [F3] gives a square root strictly larger than $∣ c ∣$ . The quadratic formula gives the positive root $z_{+} = (c + \sqrt{c^{2} + 4 A a h}) / (2 A)$ ; the other root has negative numerator $c - \sqrt{c^{2} + 4 A a h} < 0$ and positive denominator, hence is negative.

3.1A1step 2.1givenalgebra∎

Every positive solution must be one of those two quadratic roots, and only the first is positive. Substitution verifies the displayed positive root in the original equation, so it is the unique admissible step, including when $z = 0$ . AC is exactly [A1].

Depends on

Used by

Cited to discharge well-definedness by Positive Lamperti drift-implicit scheme for the CIR process.

Dependency tree · two levels

62 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

Aurélien Alfonsi, Strong convergence of some drift implicit Euler scheme. Application to the CIR process, equation (2) and the positive root following equation (3) (standard reference, not scraped)