Commit 2026-10-20 13:30 c21f0779

View on Github →

feat(Analysis/SpecialFunctions): the recurrence relation of bessel function J (#43853) This proves one of the recurrence formula for J (the other one that involves derivative will be in a separate PR). Usually the LHS is written as 2 * a * J a x / x in textbooks, but I moved x to RHS to avoid junk values on division. Also added dlmf to besselJ.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Bessel.lean

added theorem Complex.two_mul_self_mul_besselJ

Modified Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean

added theorem Complex.mul_regularizedHGFunCoeff_of_mem_right

added theorem Complex.regularizedHGFun_zero_singleton_eq_mul_add_mul

added theorem Complex.summable_pow_mul_regularizedHGFunCoeff_zero

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean