Associated relations on the full parameter space

The regularized identities of Carlson, Section 5.6, persist under analytic continuation. All Dirichlet parameters below are arbitrary complex numbers. The derivative appearing here is the derivative of the function being averaged.

theorem DirichletTransform.analyticAt_addDirichletUnit {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) : AnalyticAt ℂ (fun (c : ι → ℂ) => addDirichletUnit c i) b

Parameter shifts are translations, hence entire.

theorem DirichletTransform.IsRegCarlsonContinuation.sum_shift {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hf : ContinuousOn (fun (u : ι → ℝ) => f (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)) (b : ι → ℂ) : G b = ∑ i : ι, b i * G (addDirichletUnit b i)

Entire-parameter version of Carlson's relation 5.6-1(4).

theorem DirichletTransform.IsRegCarlsonContinuation.tangent {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {z : ι → ℂ} (hz : Set.range z ⊆ Ω) {G D : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hD : IsRegCarlsonContinuation (deriv f) z D) (b : ι → ℂ) (i j : ι) : (z i - z j) * D (addDirichletUnit (addDirichletUnit b j) i) = G (addDirichletUnit b i) - G (addDirichletUnit b j)

The tangential associated relation, with no restrictions on the parameters. The coincident-index case is included.

theorem DirichletTransform.IsRegCarlsonContinuation.tangent_sub {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {z : ι → ℂ} (hz : Set.range z ⊆ Ω) {G D : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hD : IsRegCarlsonContinuation (deriv f) z D) (b : ι → ℂ) (i j : ι) : (z i - z j) * D b = G (b - Pi.single j 1) - G (b - Pi.single i 1)

Carlson's backward-shift relation 5.6-2, in entire regularized form.

theorem DirichletTransform.IsRegCarlsonContinuation.three_node {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {z : ι → ℂ} (hz : Set.range z ⊆ Ω) {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hΩopen : IsOpen Ω) (b : ι → ℂ) (i j k : ι) : (z i - z j) * G (b - Pi.single k 1) + (z j - z k) * G (b - Pi.single i 1) + (z k - z i) * G (b - Pi.single j 1) = 0

Carlson's three-node associated relation 5.6-3. No distinctness assumptions on the nodes, indices, or Dirichlet parameters are needed.

theorem DirichletTransform.regCarlsonDirichletAverage_mul_arg {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (f : ℂ → ℂ) (hf : ContinuousOn (fun (u : ι → ℝ) => f (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)) : (regCarlsonDirichletAverage b z fun (w : ℂ) => w * f w) = ∑ i : ι, z i * (b i * regCarlsonDirichletAverage (addDirichletUnit b i) z f)

Multiplication of the function being averaged by its argument is a weighted sum of parameter shifts, on the native integral domain.

theorem DirichletTransform.IsRegCarlsonContinuation.mul_arg {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G H : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hH : IsRegCarlsonContinuation (fun (w : ℂ) => w * f w) z H) (hf : ContinuousOn (fun (u : ι → ℝ) => f (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)) (b : ι → ℂ) : H b = ∑ i : ι, z i * (b i * G (addDirichletUnit b i))

Entire-parameter multiplication-by-argument identity.

theorem DirichletTransform.IsRegCarlsonContinuation.associated {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {z : ι → ℂ} (hz : Set.range z ⊆ Ω) {G D H : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hD : IsRegCarlsonContinuation (deriv f) z D) (hH : IsRegCarlsonContinuation (fun (w : ℂ) => w * deriv f w) z H) (b : ι → ℂ) (i : ι) : G b = H (addDirichletUnit b i) - z i * D (addDirichletUnit b i) + (∑ j : ι, b j) * G (addDirichletUnit b i)

Carlson's relation 5.6-4, in regularized form on the entire parameter space. D averages f', while H averages w * f'(w).