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

Bessel differential equations and order recurrences from the series

Statement

For $z \neq 0$ , the functions in Integer-order Bessel series satisfy

$z^{2} J_{n}^{''} + z J_{n}^{'} + (z^{2} - n^{2}) J_{n} = 0, z^{2} I_{n}^{''} + z I_{n}^{'} - (z^{2} + n^{2}) I_{n} = 0.$

For real or complex $z \neq 0$ and integer $n \geq 1$ , they also satisfy

$J_{n - 1} (z) + J_{n + 1} (z) = \frac{2 n}{z} J_{n} (z), I_{n - 1} (z) - I_{n + 1} (z) = \frac{2 n}{z} I_{n} (z) .$

In addition, $J_{0}^{'} (z) = - J_{1} (z)$ .

At $z = 0$ , the series limits are $J_{0} (0) = I_{0} (0) = 1$ and $J_{n} (0) = I_{n} (0) = 0$ for $n \geq 1$ .

Facts & Assumptions

Given: The series definitions of Integer-order Bessel series and their compact-uniform convergence and termwise differentiability from Convergence and geometric tails for integer-order Bessel series.

[F1]

Integer-order Bessel series: the coefficient of degree $2 k + n$ is $(- 1)^{k} / (2^{2 k + n} k! (k + n)!)$ for $J_{n}$ and $1 / (2^{2 k + n} k! (k + n)!)$ for $I_{n}$ .

[F2]

Convergence and geometric tails for integer-order Bessel series: the series and their first two derivative series converge uniformly on compact disks.

[F3]

Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term: each defining complex power series may be differentiated term by term strictly inside its radius of convergence.

Proof

1.1F1F2F3algebra

The convergence of the first two formal derivative series in [F2], together with the infinite radius supplied by the ratio bound in Convergence and geometric tails for integer-order Bessel series, lets [F3] justify each termwise differentiation used below. For a monomial $z^{2 k + n}$ , $(z^{2} D^{2} + z D - n^{2}) z^{2 k + n} = 4 k (k + n) z^{2 k + n}$ . The coefficient ratio in [F1] is $a_{k} / a_{k - 1} = \mp 1 / [4 k (k + n)]$ for $k \geq 1$ , with the minus sign for $J_{n}$ and plus sign for $I_{n}$ . Thus the coefficient of each power cancels in the respective differential equation.

1.2F1F2F3algebra

For $J_{n - 1} + J_{n + 1}$ , reindex the $J_{n + 1}$ series so both terms have power $z^{2 k + n - 1}$ . For $k \geq 1$ their combined coefficient is $(- 1)^{k} n / [2^{2 k + n - 1} k! (k + n)!]$ , and for $k = 0$ it is $1 / [2^{n - 1} (n - 1)!]$ . These are exactly the coefficients of $(2 n / z) J_{n}$ . For $I_{n - 1} - I_{n + 1}$ the same reindexing gives the same positive combined coefficient, proving the second recurrence.

1.3F1F2F3algebra

Differentiating the $J_{0}$ series termwise by [F3] and reindexing $k = j + 1$ gives $J_{0}^{'} (z) = \sum_{j = 0}^{\infty} \frac{(- 1)^{j + 1} z^{2 j + 1}}{2^{2 j + 1} j! (j + 1)!} = - J_{1} (z) .$

2.1F1F2F3∎

Setting $z = 0$ in the convergent series leaves only the $k = 0, n = 0$ term; every term has a positive power of $z$ when $n \geq 1$ . Hence the stated limits hold.

Depends on

Used by

Dependency tree · two levels

6 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

DLMF, §10.25(i), modified Bessel differential equation (standard reference, not scraped)
DLMF, §10.2(i), Bessel differential equation (standard reference, not scraped)
DLMF, §§10.2(i), 10.6(i), and 10.25(i) (standard reference, not scraped)
N. M. Temme, “Numerical aspects of special functions,” Acta Numerica 17 (2008), §§2 and 4 (standard reference, not scraped)