Joint dependence on the exponent and Dirichlet parameters

The exponent occupies the none coordinate, and the Dirichlet parameters the some coordinates. Native joint analyticity follows from separate analyticity and a local integrable majorant. Parameter-raising relations transport it to the entire continuation.

theorem DirichletTransform.analyticOnNhd_regCarlsonRIntegral_exponent_parameters {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (p : Option ι → ℂ) => regCarlsonRIntegral (p none) (fun (i : ι) => p (some i)) z) {p : Option ι → ℂ | (fun (i : ι) => p (some i)) ∈ Complex.mvBetaConvergent}

Joint analyticity of the native regularized integral in its exponent and parameters.

theorem DirichletTransform.analyticAt_regCarlsonRContinued_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {b : E → ι → ℂ} {p : E} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hf : AnalyticAt ℂ f p) (hb : AnalyticAt ℂ b p) : AnalyticAt ℂ (fun (w : E) => regCarlsonRContinued (f w) z hz (b w)) p

The continued R-function remains analytic when the exponent and all parameters vary analytically together. Parameter raising removes every native convergence restriction.

theorem DirichletTransform.analyticOnNhd_regCarlsonRContinued_exponent_parameters {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (p : Option ι → ℂ) => regCarlsonRContinued (p none) z hz fun (i : ι) => p (some i)) Set.univ

Joint entireness of the regularized continuation in the exponent and all parameters.