TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

WKB explicit error

Statement

Adopt the hypotheses and notation of Allowed-region WKB coefficient equation: $p \in C^{2} ([a, b])$ positive, $h > 0$ , $θ (x) = \int_{a}^{x} p$ , $w_{\pm} = p^{- 1 / 2} e^{\pm i θ / h}$ , $q = \frac{3 p^{' 2}}{4 p^{2}} - \frac{p^{''}}{2 p}$ , $M$ the fundamental matrix of $(w_{+}, w_{-})$ and $c = M^{- 1} (y, y^{'})^{T}$ the coefficient curve of an exact solution $y \in C^{2} ([a, b])$ of $y^{''} + \frac{p^{2}}{h^{2}} y = 0$ . Then for every $x \in [a, b]$ :

(a) Growth bound. $∥ c (x) ∥_{1} \leq ∥ c (a) ∥_{1} \exp (h \int_{a}^{x} \frac{∣ q (s) ∣}{p (s)} d s)$ .

(b) Deviation bound. $∥ c (x) - c (a) ∥_{1} \leq ∥ c (a) ∥_{1} (\exp (h \int_{a}^{x} \frac{∣ q (s) ∣}{p (s)} d s) - 1) .$

(c) Pointwise wavefunction error. With $Ψ (x) : = c_{+} (a) w_{+} (x) + c_{-} (a) w_{-} (x)$ the leading WKB wave, $∣ y (x) - Ψ (x) ∣ \leq p (x)^{- 1 / 2} ∥ c (a) ∥_{1} (\exp (h \int_{a}^{x} \frac{∣ q (s) ∣}{p (s)} d s) - 1) .$

The estimate degenerates as $p \to 0$ (turning points are excluded by the hypotheses) and asserts nothing about connecting asymptotics across a turning point; it is an explicit finite-interval error bound of Gronwall type.

Facts & Assumptions

Given: the data of Allowed-region WKB coefficient equation, an exact solution $y \in C^{2}$ , its coefficient curve $c \in C^{1}$ , and $x \in [a, b]$ .

[F1]

$c^{'} = B c$ with $B$ continuous and $∥ B (s) ∥_{1} = h ∣ q (s) ∣ / p (s)$ ; hence $c (x) - c (a) = \int_{a}^{x} B (s) c (s) d s$ and $∥ c (x) - c (a) ∥_{1} \leq \int_{a}^{x} ∥ B (s) ∥_{1} ∥ c (s) ∥_{1} d s$ (Allowed-region WKB coefficient equation).

[F2]

Continuous scalar integrands on $[a, b]$ are Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion), their primitives have the integrand as derivative including endpoint derivatives (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive), and a $C^{1}$ function equals its initial value plus the integral of its derivative (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative). The real chain rule is The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and $d (e^{t}) / d t = e^{t}$ is the real restriction of The complex exponential is entire and its complex derivative is itself. These license the integrating factor and its integral evaluation in step 1.1, which proves the needed Gronwall bound locally without citing a separate Gronwall theorem.

[F3]

$∣ w_{\pm} (x) ∣ = p (x)^{- 1 / 2}$ , and for $c = (c_{+}, c_{-})$ one has $∣ w_{+} c_{+} + w_{-} c_{-} ∣ \leq p^{- 1 / 2} ∥ c ∥_{1}$ (Allowed-region WKB coefficient equation, algebra).

Proof

1.1F1F2algebra

[Gronwall estimate] Put $u (x) : = ∥ c (x) ∥_{1}$ and $v (s) : = ∥ B (s) ∥_{1} = h ∣ q (s) ∣ / p (s)$ . By [F1], $u (x) \leq u (a) + \int_{a}^{x} v (s) u (s) d s$ ; define $U (x) : = u (a) + \int_{a}^{x} v (s) u (s) d s$ , so $u \leq U$ , $U^{'} = v u \leq v U$ , and $\frac{d}{d x} [e^{- \int_{a}^{x} v} U (x)] \leq 0$ . Hence $u (x) \leq U (x) \leq u (a) \exp (\int_{a}^{x} v)$ , including when $u (a) = 0$ , which proves (a) directly. For (b), use the separate difference estimate in [F1] and substitute the growth bound just proved: $∥ c (x) - c (a) ∥_{1} \leq \int_{a}^{x} v (s) u (s) d s \leq u (a) \int_{a}^{x} v (s) \exp (\int_{a}^{s} v) d s = u (a) (\exp (\int_{a}^{x} v) - 1)$ , where the last equality is the fundamental theorem of calculus applied to $s \mapsto \exp (\int_{a}^{s} v)$ . This proves (b) without treating $c - c (a)$ as a homogeneous solution.

2.1step 1.1F3algebra∎

[From coefficients to values] $y (x) - Ψ (x) = w_{+} (x) (c_{+} (x) - c_{+} (a)) + w_{-} (x) (c_{-} (x) - c_{-} (a))$ , so by [F3] $∣ y (x) - Ψ (x) ∣ \leq p (x)^{- 1 / 2} ∥ c (x) - c (a) ∥_{1}$ , and inserting step 1.1 gives (c).

WKB explicit error

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources