Carlson's R-function: native integral representation

theorem DirichletTransform.regCarlsonRIntegral_natCast {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonRIntegral (↑n) b z = regCarlsonR n z b

For a natural exponent, the general-power integral is the polynomial Carlson average.