Associated Dirichlet-average identities

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

Regularized form of Carlson's relation 5.6-1(4): an average is the sum of its one-coordinate positive parameter shifts.

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

Carlson's relation 5.6-1(4) in its original normalization: an average is the weighted sum of its positive unit shifts, with weights b i / ∑ j, b j.