Aggregation of continued Dirichlet averages

Carlson's equal-node aggregation theorem holds for all complex parameters after regularization. The probability aggregation theorem supplies the identity on positive real parameters; analytic uniqueness extends it to the whole complex parameter space. The partition is surjective, so no empty blocks are inserted.

theorem DirichletTransform.sum_aggregate_dirichletParameters {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (q : ι → κ) (b : ι → ℂ) : ∑ k : κ, stdSimplexAggregate q b k = ∑ i : ι, b i

Fiber summation preserves the total parameter.

theorem DirichletTransform.carlsonAffineForm_aggregate {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (q : ι → κ) (z : κ → ℂ) (u : ι → ℝ) : carlsonAffineForm z (stdSimplexAggregate q u) = carlsonAffineForm (z ∘ q) u

The affine form factors through aggregation when nodes are constant on blocks.

theorem DirichletTransform.realCarlsonDirichletAverage_aggregate {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {q : ι → κ} (hq : Function.Surjective q) {b : ι → ℝ} (hb : b ∈ ProbabilityTheory.mvRealBetaDomain) (z : κ → ℂ) (f : ℂ → ℂ) (hf : ContinuousOn (fun (u : κ → ℝ) => f (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ κ)) : realCarlsonDirichletAverage b (z ∘ q) f = realCarlsonDirichletAverage (stdSimplexAggregate q b) z f

Real Dirichlet averages respect any surjective grouping of equal nodes.

theorem DirichletTransform.IsRegCarlsonContinuation.aggregate {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {q : ι → κ} (hq : Function.Surjective q) {f : ℂ → ℂ} {z : κ → ℂ} {G : (ι → ℂ) → ℂ} {H : (κ → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f (z ∘ q) G) (hH : IsRegCarlsonContinuation f z H) (hf : ContinuousOn (fun (u : κ → ℝ) => f (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ κ)) (b : ι → ℂ) : G b = H (stdSimplexAggregate q b)

Entire-parameter form of Carlson's Theorem 5.2-4. Equal nodes are merged and their parameters added, including zero and negative parameters.