Symmetry, aggregation, and scaling of Carlson's L-function

Carlson (1987), (2.2)–(2.5). Continued identities impose no convergence restriction on Dirichlet parameters. Positive real scaling preserves the principal branch and the right-half-plane node domain.

theorem DirichletTransform.regCarlsonLContinued_aggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] {q : ι → κ} (hq : Function.Surjective q) (t : ℂ) {z : κ → ℂ} (hz : z ∈ carlsonRVariableDomain) (b : ι → ℂ) : regCarlsonLContinued t (z ∘ q) ⋯ b = regCarlsonLContinued t z hz (stdSimplexAggregate q b)

Equation (2.4): equal nodes may be aggregated by any surjective partition.

theorem DirichletTransform.regCarlsonLContinued_option_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (t : ℂ) {b : Option ι → ℂ} (hb : b none = 0) {z : Option ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonLContinued t z hz b = regCarlsonLContinued t (z ∘ some) ⋯ (b ∘ some)

Equation (2.3): a zero parameter and its node can be deleted. The remaining index type is nonempty, as in the existing R-deletion theorem used here.

theorem DirichletTransform.regCarlsonLContinued_perm {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (σ : Equiv.Perm ι) : regCarlsonLContinued t (z ∘ ⇑σ) ⋯ (b ∘ ⇑σ) = regCarlsonLContinued t z hz b

Equation (2.2), for arbitrary complex Dirichlet parameters.

theorem DirichletTransform.regCarlsonLContinued_const {ι : Type u_1} [Fintype ι] (t w : ℂ) (hw : w ∈ carlsonRightHalfPlane) (b : ι → ℂ) : regCarlsonLContinued t (fun (x : ι) => w) ⋯ b = w ^ t * Complex.log w / Complex.Gamma (∑ i : ι, b i)

Coincident nodes reduce L to the elementary power-logarithm kernel.

@[simp]

theorem DirichletTransform.regCarlsonLContinued_one {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) : regCarlsonLContinued t (fun (x : ι) => 1) ⋯ b = 0

The all-one node vector gives zero for every exponent and parameter.

@[simp]

theorem DirichletTransform.regCarlsonLIntegral_empty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (t : ℂ) (b z : ι → ℂ) : regCarlsonLIntegral t b z = 0

The empty-index native integral vanishes.

@[simp]

theorem DirichletTransform.regCarlsonLContinued_empty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (t : ℂ) (b z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain) : regCarlsonLContinued t z hz b = 0

The entire continuation respects the empty-index convention.

theorem DirichletTransform.regCarlsonLContinued_unique {ι : Type u_1} [Fintype ι] [Unique ι] (t : ℂ) (b z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain) : regCarlsonLContinued t z hz b = z default ^ t * Complex.log (z default) / Complex.Gamma (b default)

The one-node case of Carlson's definition, with its regularizing Gamma factor.

theorem DirichletTransform.carlsonRVariableDomain_smul_pos {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℝ} (ha : 0 < a) : (fun (i : ι) => ↑a * z i) ∈ carlsonRVariableDomain

Positive real scaling preserves the node domain.

theorem DirichletTransform.regCarlsonLIntegral_smul_of_pos {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) {a : ℝ} (ha : 0 < a) : (regCarlsonLIntegral t b fun (i : ι) => ↑a * z i) = ↑a ^ t * (regCarlsonLIntegral t b z + regCarlsonRIntegral t b z * Complex.log ↑a)

Equation (2.5) for the native integral, including the logarithmic correction.

theorem DirichletTransform.regCarlsonLContinued_smul_of_pos {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℝ} (ha : 0 < a) : regCarlsonLContinued t (fun (i : ι) => ↑a * z i) ⋯ b = ↑a ^ t * (regCarlsonLContinued t z hz b + regCarlsonRContinued t z hz b * Complex.log ↑a)

Equation (2.5) for every complex Dirichlet parameter after regularization.