Joint analyticity of Carlson's single integral

The beta endpoint exponents, Dirichlet parameters, and slit-plane nodes may all vary holomorphically. A beta density with smaller positive endpoint exponents supplies the local integrable bound. This is the convergent seed for the joint continuation in §6.8.

theorem DirichletTransform.analyticOnNhd_carlsonRUnitIntervalIntegral_comp {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {U : Set (κ → ℂ)} {a a' : (κ → ℂ) → ℂ} {b z : (κ → ℂ) → ι → ℂ} (hU : IsOpen U) (ha : AnalyticOnNhd ℂ a U) (ha' : AnalyticOnNhd ℂ a' U) (hb : AnalyticOnNhd ℂ b U) (hz : AnalyticOnNhd ℂ z U) (hpos : ∀ p ∈ U, 0 < (a p).re ∧ 0 < (a' p).re) (hslit : ∀ p ∈ U, z p ∈ carlsonRSlitDomain) : AnalyticOnNhd ℂ (fun (p : κ → ℂ) => carlsonRUnitIntervalIntegral (a p) (a' p) (b p) (z p)) U

Joint analytic dependence of the beta-weighted single integral under analytic substitutions, on its endpoint convergence domain and the full product slit plane.