Symmetry, aggregation, and scaling on slit-plane nodes

Carlson (1987), (2.2)–(2.5), with arbitrary complex parameters. Positive real scaling is branch-safe on the whole slit plane; arbitrary complex scaling would require additional branch assumptions. Zero-parameter deletion retains a nonempty remaining index type. Coincident-node and singleton formulas also cover Gamma zeros in the regularized normalization.

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

Equal nodes may be combined by any surjective partition, on the full slit domain.

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

A zero parameter and its node may be deleted if at least one node remains.

theorem DirichletTransform.regCarlsonLSlit_perm {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (σ : Equiv.Perm ι) : regCarlsonLSlit t (b ∘ ⇑σ) (z ∘ ⇑σ) = regCarlsonLSlit t b z

Simultaneous permutation of nodes and parameters leaves L unchanged.

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

Coincident slit-plane nodes give the elementary power-logarithm kernel.

@[simp]

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

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

The singleton convention, including the reciprocal Gamma regularization.

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

Positive real scaling preserves the principal-branch node domain.

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

Equation (2.5) on slit-plane nodes: scaling contributes the logarithmic R-term.