Node derivatives and the Euler–Poisson system for L

The native L-integral satisfies Carlson (1987), (2.7) and (3.5). Node analyticity and the Euler–Poisson system are instances of the general Dirichlet average theorems, not independent integration-by-parts proofs.

theorem DirichletTransform.analyticOnNhd_carlsonLKernel (t : ℂ) : AnalyticOnNhd ℂ (carlsonLKernel t) Complex.slitPlane

The power-logarithm kernel is holomorphic on the principal slit plane.

theorem DirichletTransform.hasDerivAt_carlsonLKernel (t : ℂ) {w : ℂ} (hw : w ∈ Complex.slitPlane) : HasDerivAt (carlsonLKernel t) (t * carlsonLKernel (t - 1) w + w ^ (t - 1)) w

Differentiating the kernel lowers the exponent and adds a power kernel.

theorem DirichletTransform.continuousOn_carlsonLKernel_affine {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : ContinuousOn (fun (u : ι → ℝ) => carlsonLKernel t (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)

The log-power integrand is continuous on the compact simplex.

theorem DirichletTransform.analyticOnNhd_regCarlsonLIntegral_nodes {ι : Type u_1} [Fintype ι] (t : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (regCarlsonLIntegral t b) carlsonRVariableDomain

On the native convergence region, L is holomorphic jointly in all nodes.

theorem DirichletTransform.carlsonEulerPoissonOperator_regCarlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i j : ι) : carlsonEulerPoissonOperator i j b z (regCarlsonLIntegral t b) = 0

Equation (2.7): the complete Euler–Poisson system, including equal indices.

theorem DirichletTransform.regCarlsonDirichletAverage_deriv_LKernel {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonDirichletAverage b z (deriv (carlsonLKernel t)) = t * regCarlsonLIntegral (t - 1) b z + regCarlsonRIntegral (t - 1) b z

Averaging the derivative of the kernel gives the inhomogeneous lowering formula.

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i : ι) : carlsonPartialDeriv i (regCarlsonLIntegral t b) z = b i * (t * regCarlsonLIntegral (t - 1) (addDirichletUnit b i) z + regCarlsonRIntegral (t - 1) (addDirichletUnit b i) z)

Equation (3.5), in regularized form.