Holomorphic kernels in Dirichlet integrals

A kernel may depend holomorphically on extra parameters and on a complex neighborhood of the real simplex. This interface is preserved by the tangential derivatives used in Dirichlet-parameter continuation.

theorem DirichletTransform.continuousOn_complexSimplexKernel {ι : Type u_1} {κ : Type u_2} [Fintype ι] {U : Set (κ → ℂ)} {W : Set ((κ → ℂ) × (ι → ℂ))} {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : ContinuousOn H W) (hW : ∀ z ∈ U, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) : ContinuousOn (fun (p : (κ → ℂ) × (ι → ℝ)) => H (p.1, fun (i : ι) => ↑(p.2 i))) (U ×ˢ Convexity.StdSimplex.coordinateSet ℝ ι)

Joint continuity after restricting the second complex variable to real simplex coordinates.

theorem DirichletTransform.analyticOnNhd_regDirichletIntegral_kernel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {U : Set (κ → ℂ)} (hU : IsOpen U) {W : Set ((κ → ℂ) × (ι → ℂ))} {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (hW : ∀ z ∈ U, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (fun (z : κ → ℂ) => ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => H (z, fun (i : ι) => ↑(u i))) U

A native Dirichlet integral preserves holomorphic dependence on auxiliary parameters.

theorem DirichletTransform.locallyBounded_regDirichletIntegral_kernel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Finite κ] {U : Set (κ → ℂ)} (hU : IsOpen U) {F : (κ → ℂ) → (ι → ℝ) → ℂ} (hF : ContinuousOn (fun (p : (κ → ℂ) × (ι → ℝ)) => F p.1 p.2) (U ×ˢ Convexity.StdSimplex.coordinateSet ℝ ι)) {p : (ι → ℂ) × (κ → ℂ)} (hb : p.1 ∈ Complex.mvBetaConvergent) (hz : p.2 ∈ U) : ∃ (M : ℝ), ∀ᶠ (q : (ι → ℂ) × (κ → ℂ)) in nhds p, ‖ProbabilityTheory.regDirichletIntegral q.1 (F q.2)‖ ≤ M

Compactness of the kernel and a common Dirichlet majorant give local boundedness simultaneously in Dirichlet and auxiliary parameters.

theorem DirichletTransform.analyticOnNhd_regDirichletIntegral_kernel_joint {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {U : Set (κ → ℂ)} (hU : IsOpen U) {W : Set ((κ → ℂ) × (ι → ℂ))} {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (hW : ∀ z ∈ U, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) : AnalyticOnNhd ℂ (fun (p : (ι → ℂ) × (κ → ℂ)) => ProbabilityTheory.regDirichletIntegral p.1 fun (u : ι → ℝ) => H (p.2, fun (i : ι) => ↑(u i))) (Complex.mvBetaConvergent ×ˢ U)

Joint holomorphy in the native Dirichlet parameters and all auxiliary variables.