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.

Hermite recurrence

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $L^{2} = L^{2} (R, d y)$ be the complex Lebesgue space with inner product $⟨ φ, ψ ⟩ = \int_{R} φ (y) \overline{ψ (y)} d y$ linear in the first argument (The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions); this pairing makes $L^{2}$ a complex Hilbert space by $L^{2}$ with the integral pairing is a Hilbert space. For complex-valued functions, smoothness and derivatives use the componentwise convention of Complex Lp classes and Euclidean test-function conventions. Write $g_{0}$ for the function $g_{0} (y) : = π^{- 1 / 4} e^{- y^{2} / 2}$ and also for its class in $L^{2}$ . Put

$P : = {p g_{0} : p \in C [y]} \subseteq L^{2},$

the set of classes of polynomial multiples of $g_{0}$ . Each class in $P$ has a unique representative of the form $p g_{0}$ : if $p g_{0} = q g_{0}$ almost everywhere, the continuous function $(p - q) g_{0}$ vanishes almost everywhere and therefore everywhere, and $g_{0} (y) > 0$ for every $y$ , so $p = q$ . Let $Y$ be multiplication by $y$ and $\partial_{y}$ the derivative, acting on this unique smooth representative. Set $g_{- 1} : = 0$ for use in the recurrence formulas at $n = 0$ . Define

$a : = \frac{Y + \partial_{y}}{\sqrt{2}}, a^{†} : = \frac{Y - \partial_{y}}{\sqrt{2}}, g_{n} : = \frac{(a^{†})^{n} g_{0}}{\sqrt{n!}} (n \in N) .$

Then:

(a) $g_{0} \in L^{2}$ with $∥ g_{0} ∥ = 1$ ; more generally $y^{k} g_{0} \in L^{2}$ for every $k \in N$ , so $P$ is a linear subspace of $L^{2}$ all of whose members are represented by $C^{\infty}$ functions;

(b) $Y, \partial_{y}, a, a^{†}$ map $P$ into $P$ , and $\partial_{y} (p g_{0}) = (p^{'} - y p) g_{0}$ for every polynomial $p$ ;

(d) $a^{†} a - a a^{†} = - I$ on $P$ , i.e. $[a, a^{†}] = a a^{†} - a^{†} a = I$ on $P$ , and $a g_{0} = 0$ ;

(e) for every $n \in N$ : $a g_{n} = \sqrt{n} g_{n - 1}$ (with $a g_{0} = 0$ ), $a^{†} g_{n} = \sqrt{n + 1} g_{n + 1}$ , $a^{†} a g_{n} = n g_{n}$ and $a a^{†} g_{n} = (n + 1) g_{n}$ ;

(f) the polynomials

$H_{n} (y) : = (- 1)^{n} e^{y^{2}} \frac{d^{n}}{d y^{n}} e^{- y^{2}}$

are polynomials of degree $n$ with leading coefficient $2^{n}$ , $H_{0} = 1$ , $H_{1} (y) = 2 y$ , $H_{n} (- y) = (- 1)^{n} H_{n} (y)$ , and they satisfy

$H_{n}^{'} = 2 n H_{n - 1}, H_{n + 1} = 2 y H_{n} - 2 n H_{n - 1} (n \geq 1);$

moreover

$g_{n} = \frac{H_{n} g_{0}}{\sqrt{2^{n} n!}};$

(g) consequently

$\sqrt{2} y g_{n} = \sqrt{n} g_{n - 1} + \sqrt{n + 1} g_{n + 1}, \sqrt{2} g_{n}^{'} = \sqrt{n} g_{n - 1} - \sqrt{n + 1} g_{n + 1} .$

Facts & Assumptions

Given: the space $L^{2} (R, d y)$ with its inner product; the function $g_{0} (y) = π^{- 1 / 4} e^{- y^{2} / 2}$ ; the space $P$ of polynomial multiples of $g_{0}$ ; the operators $Y, \partial_{y}, a, a^{†}$ and the vectors $g_{n}$ .

[F1]

$L^{2}$ is a complex Hilbert space for $⟨ f, g ⟩ = \int f \overline{g}$ , with $∥ f ∥_{2}^{2} = \int ∣ f ∣^{2}$ ; the pairing is well defined on a.e. classes, positive definite, and satisfies $∣ ⟨ f, g ⟩ ∣ \leq \int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions, $L^{2}$ with the integral pairing is a Hilbert space, Cauchy-Schwarz inequality for $L^{2}$ ).

[F2]

For $t > 0$ , the Lebesgue Gaussian transform at dimension $n = 1$ , frequency $ξ = 0$ and parameter $t / π$ gives $\int_{R} e^{- t y^{2}} d y = \sqrt{π / t}$ ; every polynomial times a positive real Gaussian is absolutely integrable (Euclidean Gaussian transform with the 2π normalization). In particular $\int e^{- y^{2}} d y = \sqrt{π}$ and $\int e^{- y^{2} / 2} d y = \sqrt{2 π}$ .

[F3]

For $t \geq 0$ and $k \in N$ one has $t^{k} \leq 2^{k} k! e^{t / 2}$ : by The complex exponential by its power series and The complex exponential series converges absolutely for every complex argument the exponential is the sum of the absolutely convergent series $\sum_{j} (t / 2)^{j} / j!$ with nonnegative terms, so $e^{t / 2} \geq (t / 2)^{k} / k!$ .

[F4]

The real exponential is $C^{\infty}$ with $(\exp)^{'} = \exp$ (The exponential function is smooth and $(\exp)^{'} = \exp$ ); the chain rule (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 product rule (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ) hold for real-valued functions. For complex-valued functions apply those rules separately to the real and imaginary parts, as in the componentwise convention of Complex Lp classes and Euclidean test-function conventions. Consequently $(e^{- y^{2} / 2})^{'} = - y e^{- y^{2} / 2}$ and, for any complex polynomial $p$ , $(p g_{0})^{'} = (p^{'} - y p) g_{0}$ on $R$ .

[F5]

For every real $x$ , $e^{x} > 0$ and $e^{- x} = 1 / e^{x}$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ); the real exponential is strictly increasing (The exponential function is strictly increasing). The complex exponential extends the real one and satisfies $e^{z + w} = e^{z} e^{w}$ for all $z, w \in C$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[F6]

If $F : [a, b] \to R$ is differentiable at every point of $[a, b]$ and $F^{'}$ is integrable there, then $\int_{a}^{b} F^{'} = F (b) - F (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ); complex integration by parts on $R$ is valid when both derivative products are in $L^{1}$ and the product vanishes at both ends (Complex integration by parts on intervals and decaying lines). For $φ, ψ \in P$ one has $φ (y) \overline{ψ (y)} \to 0$ as $∣ y ∣ \to \infty$ , because its modulus is bounded by $C (1 + y^{2 k}) e^{- y^{2}}$ for some $C > 0$ and $k \in N$ ; [F3] bounds this by $C (1 + 2^{k} k!) e^{- y^{2} / 2}$ , which tends to zero since $e^{y^{2} / 2} \geq 1 + y^{2} / 2$ by the same nonnegative series and [F5].

Proof

1.1givenF1F2F3F5algebra

[The Gaussian moments and polynomial classes] If $p g_{0} = q g_{0}$ as $L^{2}$ classes, $(p - q) g_{0}$ is a continuous function that vanishes almost everywhere, hence vanishes everywhere; since $g_{0} > 0$ , $p = q$ . Thus the representative used to define $Y$ and $\partial_{y}$ is unique, so these operators are well defined on $P$ . By [F2], $∥ g_{0} ∥^{2} = π^{- 1 / 2} \int e^{- y^{2}} d λ = π^{- 1 / 2} \sqrt{π} = 1$ , so $g_{0} \in L^{2}$ and $∥ g_{0} ∥ = 1$ . For $k \in N$ and $y \in R$ , $∣ y^{k} g_{0} (y) ∣^{2} = π^{- 1 / 2} y^{2 k} e^{- y^{2}} \leq π^{- 1 / 2} 2^{k} k! e^{- y^{2} / 2}$ by [F3]; hence $∥ y^{k} g_{0} ∥^{2} \leq π^{- 1 / 2} 2^{k} k! \sqrt{2 π} < \infty$ by [F2], so $y^{k} g_{0} \in L^{2}$ . Every $p g_{0}$ with $\deg p = m$ is a finite linear combination of $y^{0} g_{0}, \dots, y^{m} g_{0}$ , so $p g_{0} \in L^{2}$ : $P \subseteq L^{2}$ is a linear subspace.

1.2givenF4F5algebra

[Invariance of $P$ and $a g_{0} = 0$ ] For a complex polynomial $p = p_{1} + i p_{2}$ with real polynomials $p_{1}, p_{2}$ , the real product and chain rules [F4] applied to $p_{1} g_{0}$ and $p_{2} g_{0}$ give $\partial_{y} (p g_{0}) = (p^{'} - y p) g_{0}$ ; $Y (p g_{0}) = (y p) g_{0}$ has polynomial factor $y p$ . Thus both $Y$ and $\partial_{y}$ , hence $a = (Y + \partial_{y}) / \sqrt{2}$ and $a^{†} = (Y - \partial_{y}) / \sqrt{2}$ , map $P$ into $P$ . Since $g_{0}^{'} = - y g_{0}$ by [F4], $(Y + \partial_{y}) g_{0} = y g_{0} + g_{0}^{'} = 0$ , i.e. $a g_{0} = 0$ . All members of $P$ are represented by componentwise $C^{\infty}$ functions by [F4].

1.3givenF1F2F4F5F6algebra

[Adjoint pairing] Let $φ, ψ \in P$ . They are componentwise $C^{\infty}$ by [F4], and $φ^{'} \overline{ψ}$ and $φ \overline{ψ^{'}}$ are polynomial multiples of $e^{- y^{2}}$ , hence absolutely integrable by [F2]. Their product $φ \overline{ψ}$ tends to zero at both ends by [F6]. Apply the whole-line complex integration-by-parts identity in [F6] to $u = φ$ and $v = \overline{ψ}$ to obtain $\int_{R} φ^{'} \overline{ψ} = - \int_{R} φ \overline{ψ^{'}}$ . Therefore $⟨ a^{†} φ, ψ ⟩ = 2^{- 1 / 2} \int (y φ - φ^{'}) \overline{ψ} = 2^{- 1 / 2} \int φ \overline{y ψ + ψ^{'}} = ⟨ φ, a ψ ⟩$ , since $y$ is real and $\overline{ψ^{'}}$ is the derivative of $\overline{ψ}$ ; the second identity follows by exchanging $φ$ and $ψ$ and conjugating.

1.4givenF4F5algebra

[Rodrigues polynomials] Define $H_{n} (y) : = (- 1)^{n} e^{y^{2}} \frac{d^{n}}{d y^{n}} e^{- y^{2}}$ ; each $H_{n}$ is a polynomial because differentiating $e^{- y^{2}}$ produces $e^{- y^{2}}$ times a polynomial, and $H_{0} = 1$ , $H_{1} = 2 y$ . Put $F_{n} : = e^{y^{2}} \frac{d^{n}}{d y^{n}} e^{- y^{2}}$ , so $H_{n} = (- 1)^{n} F_{n}$ . By the product rule, $F_{n + 1} = e^{y^{2}} \frac{d}{d y} (e^{- y^{2}} F_{n}) = - 2 y F_{n} + F_{n}^{'}$ , hence $H_{n + 1} = 2 y H_{n} - H_{n}^{'}$ . We prove $H_{n}^{'} = 2 n H_{n - 1}$ for all $n \geq 1$ by strong induction: for $n = 1$ this is $H_{1}^{'} = 2 = 2 H_{0}$ , and $H_{2} = 4 y^{2} - 2$ gives $H_{2}^{'} = 8 y = 4 H_{1}$ . For $n \geq 2$ , if it holds for all $1 \leq j \leq n$ , then differentiating the displayed relation at $n$ gives $H_{n + 1}^{'} = 2 H_{n} + 2 y H_{n}^{'} - H_{n}^{''}$ , while the induction hypothesis gives $H_{n}^{'} = 2 n H_{n - 1}$ and $H_{n}^{''} = 2 n H_{n - 1}^{'} = 4 n (n - 1) H_{n - 2}$ , and the same relation at $n - 1$ reads $H_{n} = 2 y H_{n - 1} - H_{n - 1}^{'}$ , so $2 y H_{n - 1} = H_{n} + 2 (n - 1) H_{n - 2}$ ; substituting, $H_{n + 1}^{'} = 2 H_{n} + 2 n (H_{n} + 2 (n - 1) H_{n - 2}) - 4 n (n - 1) H_{n - 2} = 2 (n + 1) H_{n}$ , which is the claim for $n + 1$ . Hence $H_{n}^{'} = 2 n H_{n - 1}$ for all $n \geq 1$ , and the displayed relation becomes the three-term recurrence $H_{n + 1} = 2 y H_{n} - 2 n H_{n - 1}$ for $n \geq 1$ . Induction on this recurrence gives that $H_{n}$ has degree $n$ with leading coefficient $2^{n}$ (the term $2 y H_{n}$ contributes $2 \cdot 2^{n} = 2^{n + 1}$ to $y^{n + 1}$ and $- 2 n H_{n - 1}$ only degree $n - 1$ ) and that $H_{n} (- y) = (- 1)^{n} H_{n} (y)$ , true for $n = 0, 1$ and inherited.

2.1step 1.2F4algebra

[Commutator] On any $C^{\infty}$ function $φ$ , $2 (a a^{†} - a^{†} a) = (Y + \partial_{y}) (Y - \partial_{y}) - (Y - \partial_{y}) (Y + \partial_{y})$ , and expanding with the product rule [F4] gives $(Y + \partial_{y}) (Y - \partial_{y}) = Y^{2} - Y \partial_{y} + \partial_{y} Y - \partial_{y}^{2}$ and $(Y - \partial_{y}) (Y + \partial_{y}) = Y^{2} + Y \partial_{y} - \partial_{y} Y - \partial_{y}^{2}$ ; subtracting gives $2 (\partial_{y} Y - Y \partial_{y}) = 2 I$ because $\partial_{y} (Y φ) - Y (\partial_{y} φ) = φ$ . Hence $[a, a^{†}] = I$ on $P$ by step 1.2.

2.2step 1.2step 1.4F4algebra

[Identification of $g_{n}$ ] We prove $g_{n} = H_{n} g_{0} / \sqrt{2^{n} n!}$ by induction on $n$ . For $n = 0$ this is $g_{0} = H_{0} g_{0}$ . Assume it holds for $n$ ; by step 1.2 and [F4], $(Y - \partial_{y}) (H_{n} g_{0}) = (2 y H_{n} - H_{n}^{'}) g_{0} = H_{n + 1} g_{0}$ by step 1.4, so $g_{n + 1} = a^{†} g_{n} / \sqrt{n + 1} = (Y - \partial_{y}) H_{n} g_{0} / (\sqrt{2} \sqrt{n + 1} \sqrt{2^{n} n!}) = H_{n + 1} g_{0} / \sqrt{2^{n + 1} (n + 1)!}$ , which completes the induction.

3.1step 2.1step 1.2algebra

[Ladder relations] From $[a, a^{†}] = I$ on $P$ we prove $[a, (a^{†})^{n}] = n (a^{†})^{n - 1}$ on $P$ for every $n \geq 1$ : for $n = 1$ this is step 2.1, and if it holds for $n$ then $[a, (a^{†})^{n + 1}] = [a, (a^{†})^{n}] a^{†} + (a^{†})^{n} [a, a^{†}] = n (a^{†})^{n - 1} a^{†} + (a^{†})^{n} = (n + 1) (a^{†})^{n}$ , all evaluated on $P$ , which $(a^{†})^{n}$ and $a$ preserve by step 1.2. Since $a g_{0} = 0$ , for $n \geq 1$ we get $a g_{n} = [a, (a^{†})^{n}] g_{0} / \sqrt{n!} = n (a^{†})^{n - 1} g_{0} / \sqrt{n!} = \sqrt{n} g_{n - 1}$ , while $a g_{0} = 0$ ; by definition $a^{†} g_{n} = (a^{†})^{n + 1} g_{0} / \sqrt{n!} = \sqrt{n + 1} g_{n + 1}$ for every $n$ , hence $a^{†} a g_{n} = \sqrt{n} a^{†} g_{n - 1} = n g_{n}$ and, using $a a^{†} = a^{†} a + I$ from step 2.1, $a a^{†} g_{n} = (n + 1) g_{n}$ .

4.1step 3.1step 1.4step 2.2∎

[The $y$ and $\partial_{y}$ actions] In the formulas containing $g_{n - 1}$ at $n = 0$ , set $g_{- 1} : = 0$ ; this is the zero vector, so both formulas at $n = 0$ are exactly the two ladder identities with $a g_{0} = 0$ . Since $Y = (a + a^{†}) / \sqrt{2}$ and $\partial_{y} = (a - a^{†}) / \sqrt{2}$ on $P$ by the definitions, applying step 3.1 gives $\sqrt{2} y g_{n} = a g_{n} + a^{†} g_{n} = \sqrt{n} g_{n - 1} + \sqrt{n + 1} g_{n + 1}$ and $\sqrt{2} g_{n}^{'} = a g_{n} - a^{†} g_{n} = \sqrt{n} g_{n - 1} - \sqrt{n + 1} g_{n + 1}$ . All identities are in $L^{2}$ , where equalities mean equality of classes, and the underlying functions agree pointwise because both sides are represented by continuous functions; the polynomial identities of step 1.4 are pointwise identities of polynomials.

Hermite recurrence

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources