Evaluation of Euler-type integrals by Carlson R-functions

This file is the home for the general integral evaluations of [Carl77, Section 8.1]. We first use the unit-interval parameterization; oriented complex line-segment versions can be derived from it without building phase choices into the basic definition.

noncomputable def DirichletTransform.carlsonEulerSegmentIntegral {ι : Type u_1} [Fintype ι] (a a' : ℂ) (b p q : ι → ℂ) : ℂ

The Euler-type unit-interval integral underlying Carlson's Formula 8.1-1.

Equations

• DirichletTransform.carlsonEulerSegmentIntegral a a' b p q = ∫ (u : ℝ) in Set.Ioo 0 1, ↑u ^ (a - 1) * (1 - ↑u) ^ (a' - 1) * ∏ i : ι, ((1 - ↑u) * p i + ↑u * q i) ^ (-b i)

noncomputable def DirichletTransform.carlsonEndpointRatio {ι : Type u_1} (p q : ι → ℂ) : ι → ℂ

Componentwise endpoint ratio used in Carlson's finite-segment evaluation.

Equations

• DirichletTransform.carlsonEndpointRatio p q i = q i / p i

def DirichletTransform.CompatibleCarlsonSegmentLogs {ι : Type u_1} (p q : ι → ℂ) : Prop

The principal logarithms used to factor an affine endpoint segment are compatible.

This is the exact branch condition needed for ((1-u) * p i + u * q i) ^ c = (p i) ^ c * ((1-u) + u * q i / p i) ^ c. It cannot in general be replaced by nonvanishing of the segment.

Equations

• DirichletTransform.CompatibleCarlsonSegmentLogs p q = ∀ (i : ι), ∀ u ∈ Set.Ioo 0 1, Complex.log ((1 - ↑u) * p i + ↑u * q i) = Complex.log (p i) + Complex.log (1 - ↑u + ↑u * (q i / p i))

theorem DirichletTransform.carlsonEulerSegmentIntegral_eq_rIntegral {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b p q : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hb : b ∈ Complex.mvBetaConvergent) (hp : ∀ (i : ι), p i ≠ 0) (hsegment : ∀ (i : ι), ∀ u ∈ Set.Icc 0 1, (1 - ↑u) * p i + ↑u * q i ≠ 0) (hlog : CompatibleCarlsonSegmentLogs p q) (hratio : carlsonEndpointRatio p q ∈ carlsonRVariableDomain) : carlsonEulerSegmentIntegral a a' b p q = (a.betaIntegral a' * ∏ i : ι, p i ^ (-b i)) * carlsonRIntegral (-a) b (carlsonEndpointRatio p q)

Carlson's Formula 8.1-1 in unit-interval form, with the principal-log compatibility hypothesis needed to extract the endpoint powers.

noncomputable def DirichletTransform.carlsonEulerRayIntegral {ι : Type u_1} [Fintype ι] (a : ℂ) (b p w : ι → ℂ) : ℂ

The ray integral underlying Carlson's Formulas 8.1-2 and 8.1-3. The choice of endpoint values p and ray directions w accommodates either orientation.

Equations

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

def DirichletTransform.CompatibleCarlsonRayLogs {ι : Type u_1} (p w : ι → ℂ) : Prop

The principal logarithms used to factor a Carlson ray are compatible.

Equations

• DirichletTransform.CompatibleCarlsonRayLogs p w = ∀ (i : ι) (s : ℝ), 0 < s → Complex.log (p i + ↑s * w i) = Complex.log (w i) + Complex.log (p i / w i + ↑s)

theorem DirichletTransform.carlsonEulerRayIntegral_eq_rIntegral {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b p w : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hb : b ∈ Complex.mvBetaConvergent) (hw : ∀ (i : ι), w i ≠ 0) (hray : ∀ (i : ι) (s : ℝ), 0 ≤ s → p i + ↑s * w i ≠ 0) (hlog : CompatibleCarlsonRayLogs p w) (hvars : (fun (i : ι) => p i / w i) ∈ carlsonRVariableDomain) : carlsonEulerRayIntegral a b p w = (a.betaIntegral a' * ∏ i : ι, w i ^ (-b i)) * carlsonRIntegral (-a') b fun (i : ι) => p i / w i

Carlson's Formulas 8.1-2 and 8.1-3, with the principal-log compatibility hypothesis needed to extract the ray-direction powers.