Dirichlet continuation with holomorphic auxiliary parameters

Complexifying the simplex coordinates makes tangential differentiation compatible with holomorphic dependence on auxiliary variables. The finite parameter-shift construction can therefore be used jointly, rather than independently for each auxiliary parameter.

noncomputable def DirichletTransform.complexSimplexTangentDeriv {ι : Type u_1} {κ : Type u_2} (j i : ι) (H : (κ → ℂ) × (ι → ℂ) → ℂ) (p : (κ → ℂ) × (ι → ℂ)) : ℂ

A tangential derivative in the complexified simplex coordinates, leaving the auxiliary parameter block fixed.

Equations

• DirichletTransform.complexSimplexTangentDeriv j i H p = (fderiv ℂ H p) (0, Pi.single j 1 - Pi.single i 1)

theorem DirichletTransform.analyticOnNhd_complexSimplexTangentDeriv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {W : Set ((κ → ℂ) × (ι → ℂ))} {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (j i : ι) : AnalyticOnNhd ℂ (complexSimplexTangentDeriv j i H) W

Complex tangential differentiation preserves joint analyticity.

theorem DirichletTransform.contDiffNearStdSimplex_complexKernel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {W : Set ((κ → ℂ) × (ι → ℂ))} (hWo : IsOpen W) {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (z : κ → ℂ) (hW : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) (N : ℕ) : ContDiffNearStdSimplex N fun (u : ι → ℝ) => H (z, fun (i : ι) => ↑(u i))

Restriction of a holomorphic kernel is smooth near the real simplex.

theorem DirichletTransform.complexSimplexTangentDeriv_eq_real {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {W : Set ((κ → ℂ) × (ι → ℂ))} {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (z : κ → ℂ) {u : ι → ℝ} (hu : (z, fun (i : ι) => ↑(u i)) ∈ W) (j i : ι) : complexSimplexTangentDeriv j i H (z, fun (k : ι) => ↑(u k)) = stdSimplexTangentDeriv j i (fun (v : ι → ℝ) => H (z, fun (k : ι) => ↑(v k))) u

The complexified tangent derivative agrees with the real tangent derivative used in the simplex integration-by-parts theorem.

def DirichletTransform.shiftedComplexKernelIntegral {ι : Type u_1} {κ : Type u_2} [Fintype ι] (i : ι) : List { j : ι // j ≠ i } → ((κ → ℂ) × (ι → ℂ) → ℂ) → (ι → ℂ) × (κ → ℂ) → ℂ

Tangential parameter shifts, retaining a jointly holomorphic kernel.

Equations

• One or more equations did not get rendered due to their size.
• DirichletTransform.shiftedComplexKernelIntegral i [] x✝¹ x✝ = ProbabilityTheory.regDirichletIntegral x✝.1 fun (u : ι → ℝ) => x✝¹ (x✝.2, fun (k : ι) => ↑(u k))

theorem DirichletTransform.analyticOnNhd_shiftedComplexKernelIntegral {ι : 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) (i : ι) (l : List { j : ι // j ≠ i }) : AnalyticOnNhd ℂ (shiftedComplexKernelIntegral i l H) (shiftRegion i l ×ˢ U)

Every finite shift expression is jointly holomorphic on its convergence region.

theorem DirichletTransform.shiftedComplexKernelIntegral_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {W : Set ((κ → ℂ) × (ι → ℂ))} (hWo : IsOpen W) {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (z : κ → ℂ) (hW : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) (i : ι) (l : List { j : ι // j ≠ i }) {b : ι → ℂ} (hb : ∀ (k : ι), ↑l.length + 2 < (b k).re) : shiftedComplexKernelIntegral i l H (b, z) = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => H (z, fun (k : ι) => ↑(u k))

The finite shift expression agrees with the native integral sufficiently far inside the convergence region. This is the integration-by-parts identification used for gluing.

theorem DirichletTransform.exists_joint_regDirichletContinuation_kernel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (N : ℕ) {U : Set (κ → ℂ)} (hU : IsOpen U) {W : Set ((κ → ℂ) × (ι → ℂ))} (hWo : IsOpen W) {H : (κ → ℂ) × (ι → ℂ) → ℂ} (hH : AnalyticOnNhd ℂ H W) (hW : ∀ z ∈ U, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, (z, fun (i : ι) => ↑(u i)) ∈ W) : ∃ (F : (ι → ℂ) × (κ → ℂ) → ℂ), AnalyticOnNhd ℂ F (dirichletConvergenceRegion N ×ˢ U) ∧ ∀ z ∈ U, Set.EqOn (fun (b : ι → ℂ) => F (b, z)) (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => H (z, fun (i : ι) => ↑(u i))) Complex.mvBetaConvergent

Finite-order continuation, jointly in Dirichlet and auxiliary parameters.

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

The finite shift constructions glue to a continuation entire in the Dirichlet parameters and jointly holomorphic with the auxiliary parameters.