Modified Bessel functions of the first kind

DefinitionTerms of the modified Bessel series#✓fully proved

For natural numbers \(m, k\) and a real number \(x\), the \(k\)-th term of the series for the modified Bessel function of the first kind of order \(m\) is \(x^{2k+m} / (2^{2k+m} \, k! \, (k+m)!)\).

noncomputable def modifiedBesselI_term (m k : ℕ) (x : ℝ) : ℝ :=
  x ^ (2 * k + m) /
    ((2 : ℝ) ^ (2 * k + m) * (Nat.factorial k : ℝ) * (Nat.factorial (k + m) : ℝ))

Used by 1

Used byModified Bessel function of the first kind

DefinitionModified Bessel function of the first kind#✓fully proved

For a natural number \(m\) and real \(x\), the modified Bessel function of the first kind of order \(m\) is \(I_m(x) = \sum_{k \ge 0} x^{2k+m} / (2^{2k+m} \, k! \, (k+m)!)\).

noncomputable def modifiedBesselI (m : ℕ) (x : ℝ) : ℝ :=
  ∑' k : ℕ, modifiedBesselI_term m k x

Uses 1 · Used by 2

Statement usesTerms of the modified Bessel series

Used byModified Bessel function of the first kind of order one · Modified Bessel function of the first kind of order zero

DefinitionModified Bessel function of the first kind of order zero#✓fully proved

For a real number \(x\), \(I_0(x)\) is the modified Bessel function of the first kind of order \(0\) at \(x\), that is, \(I_0(x) = \sum_{k \ge 0} x^{2k} / (2^{2k} \, (k!)^2)\).

noncomputable def modifiedBesselI_zero (x : ℝ) : ℝ :=
  modifiedBesselI 0 x

Uses 1

Statement usesModified Bessel function of the first kind

DefinitionModified Bessel function of the first kind of order one#✓fully proved

For a real number \(x\), \(I_1(x)\) is the modified Bessel function of the first kind of order \(1\) at \(x\), that is, \(I_1(x) = \sum_{k \ge 0} x^{2k+1} / (2^{2k+1} \, k! \, (k+1)!)\).

noncomputable def modifiedBesselI_one (x : ℝ) : ℝ :=
  modifiedBesselI 1 x

Uses 1

Statement usesModified Bessel function of the first kind

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.