Unit-interval kernel and near-one series representation

noncomputable def DirichletTransform.carlsonRUnitIntervalIntegral {ι : Type u_1} [Fintype ι] (a a' : ℂ) (b z : ι → ℂ) : ℂ

The beta-weighted unit-interval integral in Carlson's single-integral representation.

Equations

• DirichletTransform.carlsonRUnitIntervalIntegral a a' b z = ∫ (u : ℝ) in Set.Ioo 0 1, ↑u ^ (a - 1) * (1 - ↑u) ^ (a' - 1) * ∏ i : ι, (1 - ↑u + ↑u * z i) ^ (-b i)

theorem DirichletTransform.hasSum_regCarlsonRIntegral_near_one {ι : Type u_1} [Fintype ι] (a : ℂ) (b y : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) (hy : ∀ (i : ι), ‖y i‖ < 1) : HasSum (fun (n : ℕ) => Polynomial.eval a (ascPochhammer ℂ n) / ↑n.factorial * regCarlsonR n y b) (regCarlsonRIntegral (-a) b fun (i : ι) => 1 - y i)

The regularized R-integral has its R-polynomial expansion near the all-one variable.

theorem DirichletTransform.carlsonRUnitIntervalIntegral_eq_of_norm_one_sub_lt_one {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hb : b ∈ Complex.mvBetaConvergent) (hz : ∀ (i : ι), ‖1 - z i‖ < 1) : carlsonRUnitIntervalIntegral a a' b z = a.betaIntegral a' * carlsonRIntegral (-a) b z

Carlson's single-integral identity in the polydisc centered at the all-one variable.