The unit-interval representation and node analyticity

theorem DirichletTransform.affineSegment_mem_rightHalfPlane {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (i : ι) : 1 - ↑u + ↑u * z i ∈ carlsonRightHalfPlane

The affine segment from 1 to a point in Carlson's right-half-plane domain remains in that domain.

noncomputable def DirichletTransform.singleIntegralKernel {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (u : ℝ) : ℂ

The product kernel in Carlson's single-integral formula.

Equations

• DirichletTransform.singleIntegralKernel b z u = ∏ i : ι, (1 - ↑u + ↑u * z i) ^ (-b i)

theorem DirichletTransform.continuousOn_singleIntegralKernel_fixed {ι : Type u_1} [Fintype ι] (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ContinuousOn (singleIntegralKernel b z) (Set.Icc 0 1)

At fixed Carlson variables in the slit plane, the product kernel is continuous on the closed unit interval.

theorem DirichletTransform.analyticOnNhd_carlsonRUnitIntervalIntegral_slit {ι : Type u_1} [Fintype ι] (a a' : ℂ) (b : ι → ℂ) (ha : 0 < a.re) (ha' : 0 < a'.re) : AnalyticOnNhd ℂ (carlsonRUnitIntervalIntegral a a' b) carlsonRSlitDomain

For positive beta exponents, the unit-interval integral is analytic in all Carlson variables throughout the full product slit plane (Carlson's Theorem 6.8-1).

theorem DirichletTransform.analyticOnNhd_carlsonRUnitIntervalIntegral {ι : Type u_1} [Fintype ι] (a a' : ℂ) (b : ι → ℂ) (ha : 0 < a.re) (ha' : 0 < a'.re) : AnalyticOnNhd ℂ (carlsonRUnitIntervalIntegral a a' b) carlsonRVariableDomain

The right-half-plane restriction of the slit-plane analyticity theorem.

theorem DirichletTransform.carlsonRUnitIntervalIntegral_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) : carlsonRUnitIntervalIntegral a a' b z = a.betaIntegral a' * carlsonRIntegral (-a) b z

Carlson's Theorem 6.8-1 in unit-interval form. The homogeneity relation a + a' = ∑ i, b i supplies the exponent at the endpoint u = 1.