Euler--Poisson equations for Carlson's Dirichlet averages

Tangential integration by parts proves the Euler--Poisson system first for large real parts of the parameters. Analytic uniqueness extends it to the native convergence domain.

theorem DirichletTransform.regCarlsonDirichletAverage_tangent {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i j : ι) (hij : i ≠ j) : (z i - z j) * regCarlsonDirichletAverage (addDirichletUnit (addDirichletUnit b j) i) z (deriv f) = regCarlsonDirichletAverage (addDirichletUnit b i) z f - regCarlsonDirichletAverage (addDirichletUnit b j) z f

The tangential contiguous relation, on the native convergence domain.

theorem DirichletTransform.carlsonEulerPoissonOperator_regCarlsonDirichletAverage {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i j : ι) : (carlsonEulerPoissonOperator i j b z fun (w : ι → ℂ) => regCarlsonDirichletAverage b w f) = 0

Carlson 5.4-1, regularized form. A regularized Carlson average of a function holomorphic on a convex domain satisfies the Euler--Poisson system on node vectors contained in that domain.

theorem DirichletTransform.carlsonEulerPoissonOperator_carlsonDirichletAverage {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i j : ι) : (carlsonEulerPoissonOperator i j b z fun (w : ι → ℂ) => Complex.Gamma (∑ k : ι, b k) * regCarlsonDirichletAverage b w f) = 0

Carlson 5.4-1. The native Carlson Dirichlet average satisfies the Euler--Poisson system on its convergence domain.