The full Euler–Poisson system for Carlson's L-function #
Carlson (1987), (2.7), for all complex parameters and all slit-plane nodes. Joint holomorphy of the second node derivatives permits continuation first in the parameters and then in the nodes. Equal indices and coincident nodes are included.
theorem
DirichletTransform.analyticAt_carlsonEulerPoissonOperator_regCarlsonLSlit_comp
{ι : Type u_1}
[Fintype ι]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{t : E → ℂ}
{b z : E → ι → ℂ}
{p : E}
(ht : AnalyticAt ℂ t p)
(hb : AnalyticAt ℂ b p)
(hz : AnalyticAt ℂ z p)
(hslit : z p ∈ carlsonRSlitDomain)
(i j : ι)
:
AnalyticAt ℂ (fun (q : E) => carlsonEulerPoissonOperator i j (b q) (z q) (regCarlsonLSlit (t q) (b q))) p
The entire Euler–Poisson expression is jointly holomorphic in all its arguments.
theorem
DirichletTransform.carlsonEulerPoissonOperator_regCarlsonLSlit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i j : ι)
:
Carlson (1987), (2.7), without convergence restrictions or node-separation assumptions.
theorem
DirichletTransform.carlsonEulerPoissonOperator_carlsonLSlit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRSlitDomain)
(i j : ι)
:
The ordinary normalization satisfies the same homogeneous PDE wherever it represents the ordinary function; the identity also holds for Lean's totalization at Gamma poles.