Positive-ray representation and its change of variables

noncomputable def DirichletTransform.carlsonRPositiveRayIntegral {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) : ℂ

The positive-ray form of Carlson's single-integral representation.

Equations

• DirichletTransform.carlsonRPositiveRayIntegral a b z = ∫ (s : ℝ) in Set.Ioi 0, ↑s ^ (a - 1) * ∏ i : ι, (z i + ↑s) ^ (-b i)

theorem DirichletTransform.carlsonRPositiveRayIntegral_eq_unitInterval {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (hsum : a + a' = ∑ i : ι, b i) (hz : z ∈ carlsonRVariableDomain) : carlsonRPositiveRayIntegral a b z = carlsonRUnitIntervalIntegral a' a b z

Under the balancing relation, reciprocal translation identifies the positive-ray integral with the unit-interval integral having its beta exponents interchanged.

theorem DirichletTransform.carlsonRPositiveRayIntegral_eq {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : carlsonRPositiveRayIntegral a b z = a.betaIntegral a' * carlsonRIntegral (-a') b z

Carlson's Theorem 6.8-1 in positive-ray form.

theorem DirichletTransform.carlsonRPositiveRayIntegral_eq_gamma_mul_continued {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hz : z ∈ carlsonRVariableDomain) : carlsonRPositiveRayIntegral a b z = Complex.Gamma a * Complex.Gamma a' * regCarlsonRContinued (-a') z hz b

The positive-ray representation with no individual Dirichlet-parameter restrictions; only the two endpoint convergence conditions remain.