Documentation

LeanPool.CarlsonFunctions.Carlson.L.SlitRelations

Associated relations for L on the full product slit plane #

Carlson (1987), (2.6), (3.1)–(3.4), and (3.7), for arbitrary complex exponents and Dirichlet parameters. The identities are regularized and have no exceptional parameter hyperplanes. Euler inversion retains the minus sign from the reflected exponent, and the lowering and tangent identities retain their inhomogeneous R-terms.

theorem DirichletTransform.regCarlsonLSlit_eq_sum_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) :
regCarlsonLSlit t b z = ∑ i : ι, b i * regCarlsonLSlit t (addDirichletUnit b i) z

Equation (3.1) on slit-plane nodes.

theorem DirichletTransform.regCarlsonLSlit_add_one_eq_sum_mul_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) :
regCarlsonLSlit (t + 1) b z = ∑ i : ι, b i * z i * regCarlsonLSlit t (addDirichletUnit b i) z

Equation (3.2) on slit-plane nodes.

theorem DirichletTransform.regCarlsonLSlit_eq_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i : ι) :
regCarlsonLSlit t b z = (∑ j : ι, b j + t) * regCarlsonLSlit t (addDirichletUnit b i) z - t * z i * regCarlsonLSlit (t - 1) (addDirichletUnit b i) z + regCarlsonRSlit t (addDirichletUnit b i) z - z i * regCarlsonRSlit (t - 1) (addDirichletUnit b i) z

Equation (3.4), in its division-free parameter-raised form.

theorem DirichletTransform.regCarlsonLSlit_euler {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) :
regCarlsonLSlit t b z = (-∏ i : ι, z i ^ (-b i)) * regCarlsonLSlit (-∑ i : ι, b i - t) b fun (i : ι) => (z i)⁻¹

Equation (2.6): Euler inversion on the full slit domain.

theorem DirichletTransform.regCarlsonLSlit_three_node {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i j k : ι) :
(z i - z j) * regCarlsonLSlit t (b - Pi.single k 1) z + (z j - z k) * regCarlsonLSlit t (b - Pi.single i 1) z + (z k - z i) * regCarlsonLSlit t (b - Pi.single j 1) z = 0

Equation (3.3), allowing coincident indices and nodes.

theorem DirichletTransform.regCarlsonLSlit_tangent_sub {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i j : ι) :
(z i - z j) * (t * regCarlsonLSlit (t - 1) b z + regCarlsonRSlit (t - 1) b z) = regCarlsonLSlit t (b - Pi.single j 1) z - regCarlsonLSlit t (b - Pi.single i 1) z

Equation (3.7), with its R-term and without parameter restrictions.

theorem DirichletTransform.regCarlsonLSlit_sub_dirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i : ι) :
regCarlsonLSlit t (b - Pi.single i 1) z = (∑ j : ι, b j + t - 1) * regCarlsonLSlit t b z - t * z i * regCarlsonLSlit (t - 1) b z + regCarlsonRSlit t b z - z i * regCarlsonRSlit (t - 1) b z

Equation (3.4) in parameter-lowered form. Regularization eliminates the ordinary normalization's factor c - 1, so no exceptional parameter is excluded.

theorem DirichletTransform.regCarlsonLSlit_weighted_tangent_sub {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i j : ι) :
(∑ k : ι, b k + t - 1) * (z i - z j) * regCarlsonLSlit t b z + z j * regCarlsonLSlit t (b - Pi.single i 1) z - z i * regCarlsonLSlit t (b - Pi.single j 1) z + (z i - z j) * regCarlsonRSlit t b z = 0

Carlson (1987), (3.8), on the full slit domain. The undivided identity includes coincident nodes and equal indices.