Bessel function

We introduce Bessel functions in this file. Bessel functions commonly take two complex parameters a and x. They are analytic for x ∈ Complex.slitPlane. We also provide scoped notation in the namespace Complex for these functions.

Complex.besselJ a x: Bessel function of the first kind $J_a(x)$

The Bessel function $J_a(x)$ has the representation $$ J_a(x) = (x / 2)^a \frac{₀F₁(-; a + 1; -(x/2)^2)} {Γ(a + 1)} $$ where $₀F₁$ is the hypergeometric function. Based on this, we define Complex.besselJ a x using Complex.regularizedHGFun for the fraction part which removes the singularity for negative integer $a$.

This function is analytic for all x when a is an integer. (see Complex.analyticAt_besselJ_int)

$J_a(0) = 0$ for all complex $a \ne 0$. For $a = 0$, we have $J_0(0) = 1$. (See Complex.besselJ_zero)

TODO

• Bessel function of the second kind
• Differential equations
• Generating functions
• Bessel's integrals

noncomputable def Complex.besselJ (a x : ℂ) : ℂ

Bessel function of the first kind $J_a(x)$.

Equations

• Complex.besselJ a x = (x / 2) ^ a * Complex.regularizedHGFun 0 {a + 1} (-(x / 2) ^ 2)

theorem Complex.besselJ_def : besselJ = fun (a x : ℂ) => (x / 2) ^ a * regularizedHGFun 0 {a + 1} (-(x / 2) ^ 2)

theorem Complex.besselJ_int_neg (a : ℤ) (x : ℂ) : besselJ (↑a) (-x) = (-1) ^ a * besselJ (↑a) x

J a is even or odd when $a$ is even or odd, respectively.

theorem Complex.odd_besselJ {a : ℤ} (ha : Odd a) : Function.Odd (besselJ ↑a)

theorem Complex.even_besselJ {a : ℤ} (ha : Even a) : Function.Even (besselJ ↑a)

theorem Complex.analyticAt_besselJ (a : ℂ) {x : ℂ} (h : x ∈ slitPlane) : AnalyticAt ℂ (besselJ a) x

J a is analytic outside of the branch cut on the negative real axis.

theorem Complex.analyticOnNhd_besselJ (a : ℂ) : AnalyticOnNhd ℂ (besselJ a) slitPlane

theorem Complex.besselJ_neg_int (a : ℤ) (x : ℂ) : besselJ (-↑a) x = (-1) ^ a * besselJ (↑a) x

For integer a, J a and J (-a) are related by a sign.

theorem Complex.besselJ_neg_comm (a : ℤ) (x : ℂ) : besselJ (-↑a) x = besselJ (↑a) (-x)

theorem Complex.analyticAt_besselJ_int (a : ℤ) (x : ℂ) : AnalyticAt ℂ (besselJ ↑a) x

J a is analytic for integer a.

theorem Complex.analyticOnNhd_besselJ_int (a : ℤ) : AnalyticOnNhd ℂ (besselJ ↑a) Set.univ

theorem Complex.besselJ_zero (a : ℂ) : besselJ a 0 = if a = 0 then 1 else 0