Associated R-relations on the full slit domain #
theorem
DirichletTransform.regCarlsonRSlit_eq_addDirichletUnit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i : ι)
:
regCarlsonRSlit t b z = (∑ j : ι, b j + t) * regCarlsonRSlit t (addDirichletUnit b i) z - t * z i * regCarlsonRSlit (t - 1) (addDirichletUnit b i) z
The parameter-raising identity on the full slit domain, without dividing by the exponent or total parameter.
theorem
DirichletTransform.regCarlsonRSlit_sub_dirichletUnit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i : ι)
:
regCarlsonRSlit t (b - Pi.single i 1) z = (∑ j : ι, b j + t - 1) * regCarlsonRSlit t b z - t * z i * regCarlsonRSlit (t - 1) b z
Parameter lowering without dividing by the total parameter minus one.
theorem
DirichletTransform.regCarlsonRSlit_tangent_sub
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i j : ι)
:
(z i - z j) * (t * regCarlsonRSlit (t - 1) b z) = regCarlsonRSlit t (b - Pi.single j 1) z - regCarlsonRSlit t (b - Pi.single i 1) z
The backward-shift tangential relation, including equal indices and coincident nodes.
theorem
DirichletTransform.regCarlsonRSlit_tangent
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i j : ι)
:
(z i - z j) * (t * regCarlsonRSlit (t - 1) (addDirichletUnit (addDirichletUnit b j) i) z) = regCarlsonRSlit t (addDirichletUnit b i) z - regCarlsonRSlit t (addDirichletUnit b j) z
The parameter-raised tangential relation on the full slit domain.