← Mathematical handbook

noncomputable def Verification.eulerHypergeometric (a b c z : ℝ) : ℝ

Euler's integral representation, with the normalization in equation (26). The paper uses it where 0 < a < c and z ≤ 0.

Equations

• Verification.eulerHypergeometric a b c z = Real.Gamma c / (Real.Gamma a * Real.Gamma (c - a)) * ∫ (t : ℝ) in 0..1, t ^ (a - 1) * (1 - t) ^ (c - a - 1) * (1 - t * z) ^ (-b)

theorem Verification.eulerHypergeometric_successor {a : ℝ} (ha : 0 < a) (b z : ℝ) : eulerHypergeometric a b (a + 1) z = a * ∫ (t : ℝ) in 0..1, t ^ (a - 1) * (1 - t * z) ^ (-b)