Node and joint analyticity of native Dirichlet averages

theorem DirichletTransform.analyticOnNhd_regCarlsonDirichletAverage_nodes {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (fun (z : ι → ℂ) => regCarlsonDirichletAverage b z f) {z : ι → ℂ | Set.range z ⊆ Ω}

Carlson 5.3-3, node-variable part. On a convex domain of holomorphy, a regularized Carlson average is analytic in all node variables throughout the corresponding product domain.

theorem DirichletTransform.locallyBounded_regCarlsonDirichletAverage_parameters_nodes {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : ContinuousOn f Ω) {p : (ι → ℂ) × (ι → ℂ)} (hb : p.1 ∈ Complex.mvBetaConvergent) (hz : Set.range p.2 ⊆ Ω) : ∃ (M : ℝ), ∀ᶠ (q : (ι → ℂ) × (ι → ℂ)) in nhds p, ‖regCarlsonDirichletAverage q.1 q.2 f‖ ≤ M

A common integrable Dirichlet majorant bounds the average near each parameter and node vector. No continuity of the density at the simplex boundary is required.

theorem DirichletTransform.analyticOnNhd_regCarlsonDirichletAverage_parameters_nodes {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) : AnalyticOnNhd ℂ (fun (p : (ι → ℂ) × (ι → ℂ)) => regCarlsonDirichletAverage p.1 p.2 f) {p : (ι → ℂ) × (ι → ℂ) | p.1 ∈ Complex.mvBetaConvergent ∧ Set.range p.2 ⊆ Ω}

Carlson 5.3-3, joint form. Separate analyticity and a local integral bound give joint analyticity by the locally bounded Osgood theorem.