Native Carlson S-integrals

noncomputable def DirichletTransform.regCarlsonSIntegral {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) : ℂ

The native regularized integral representing S(b,z) / Γ(∑ i, b i) when all Dirichlet parameters have positive real part.

Equations

• DirichletTransform.regCarlsonSIntegral b z = DirichletTransform.regCarlsonDirichletAverage b z Complex.exp

theorem DirichletTransform.analyticOnNhd_exp_carlsonAffineForm {ι : Type u_1} [Fintype ι] (u : ι → ℝ) : AnalyticOnNhd ℂ (fun (z : ι → ℂ) => Complex.exp (carlsonAffineForm z u)) Set.univ

For each simplex point, the exponential Carlson kernel is entire in all z variables.

theorem DirichletTransform.hasDerivAt_exp_carlsonAffineForm_update {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) (i : ι) : HasDerivAt (fun (w : ℂ) => Complex.exp (carlsonAffineForm (Function.update z i w) u)) (↑(u i) * Complex.exp (carlsonAffineForm z u)) (z i)

Varying coordinate i of z, the derivative of the exponential Carlson kernel is the kernel multiplied by the simplex coordinate u i.

theorem DirichletTransform.hasDerivAt_regCarlsonSIntegral_update {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) : HasDerivAt (fun (w : ℂ) => regCarlsonSIntegral b (Function.update z i w)) (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * Complex.exp (carlsonAffineForm z u)) (z i)

Coordinate differentiation of the native regularized S integral. This is the specialization of Carlson's differentiation formula to the exponential kernel.

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonSIntegral {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) : carlsonPartialDeriv i (regCarlsonSIntegral b) z = b i * regCarlsonSIntegral (addDirichletUnit b i) z

Carlson's coordinate differentiation formula for the regularized native S integral: differentiation in z i raises the corresponding Dirichlet parameter.

theorem DirichletTransform.iteratedDeriv_cexp_eq (n : ℕ) : iteratedDeriv n Complex.exp = Complex.exp

Every iterated complex derivative of the exponential function is the exponential function itself.

theorem DirichletTransform.regCarlsonDirichletAverage_iteratedDeriv_exp {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) : regCarlsonDirichletAverage b z (iteratedDeriv n Complex.exp) = regCarlsonSIntegral b z

Carlson's Theorem 5.8-2 in regularized integral form: replacing the averaged exponential by any of its iterated derivatives does not change the S integral. Carlson denotes the left-hand side by S⁽ⁿ⁾ and writes S⁽ⁿ⁾ = S.

noncomputable def DirichletTransform.carlsonSIntegral {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) : ℂ

Carlson's native, unregularized S integral. Its intended integral interpretation requires b ∈ Complex.mvBetaConvergent.

Equations

• DirichletTransform.carlsonSIntegral b z = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonSIntegral b z

theorem DirichletTransform.carlsonSIntegral_eq_Gamma_mul_reg {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) : carlsonSIntegral b z = Complex.Gamma (∑ i : ι, b i) * regCarlsonSIntegral b z

The unregularized and regularized native S integrals differ by Γ(∑ i, b i).

theorem DirichletTransform.carlsonDirichletAverage_iteratedDeriv_exp {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) : Complex.Gamma (∑ i : ι, b i) * regCarlsonDirichletAverage b z (iteratedDeriv n Complex.exp) = carlsonSIntegral b z

Carlson's Theorem 5.8-2 for the unregularized native integral.