Carlson's R-function: analyticity and differentiation

This file proves the pointwise kernel identities, differentiation under the Dirichlet integral, and joint analyticity in the nodes for Carlson's Theorem 5.9-2 on the native parameter convergence region and right-half-plane node domain.

theorem DirichletTransform.analyticOnNhd_cpow_carlsonAffineForm {ι : Type u_1} [Fintype ι] (t : ℂ) (u : ι → ℝ) (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : AnalyticOnNhd ℂ (fun (z : ι → ℂ) => carlsonAffineForm z u ^ t) carlsonRVariableDomain

For a fixed simplex point, Carlson's power kernel is analytic in all variables throughout the right-half-plane domain. This is the pointwise input to the analyticity in Theorem 5.9-2.

theorem DirichletTransform.hasDerivAt_cpow_carlsonAffineForm_update {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) (i : ι) : HasDerivAt (fun (w : ℂ) => carlsonAffineForm (Function.update z i w) u ^ t) (↑(u i) * (t * carlsonAffineForm z u ^ (t - 1))) (z i)

The coordinate derivative of Carlson's power kernel. This is the pointwise form of Relation 5.9-6, equation (9).

theorem DirichletTransform.update_mem_carlsonRVariableDomain_of_mem_closedBall {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i : ι) {w : ℂ} (hw : w ∈ Metric.closedBall (z i) ((z i).re / 2)) : Function.update z i w ∈ carlsonRVariableDomain

A sufficiently small closed ball around one coordinate of a point in the Carlson right-half-plane domain remains in that domain after updating that coordinate.

theorem DirichletTransform.hasDerivAt_regCarlsonRIntegral_update {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i : ι) : HasDerivAt (fun (w : ℂ) => regCarlsonRIntegral t b (Function.update z i w)) (t * b i * regCarlsonRIntegral (t - 1) (addDirichletUnit b i) z) (z i)

Carlson's first differentiation formula, Relation 5.9-6, equation (9), for the native regularized R integral.

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i : ι) : carlsonPartialDeriv i (regCarlsonRIntegral t b) z = t * b i * regCarlsonRIntegral (t - 1) (addDirichletUnit b i) z

Coordinate form of Carlson's first differentiation formula, Relation 5.9-6, equation (9).

theorem DirichletTransform.analyticOnNhd_regCarlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (regCarlsonRIntegral t b) carlsonRVariableDomain

Carlson's joint analyticity assertion in Theorem 5.9-2, restricted to the nodes, for the native regularized integral on the right-half-plane variable domain.

The coordinate differentiation theorem above supplies the derivatives. The analytic-under-the-integral argument is stated jointly because this is the form needed for the identity principle and for the differential equations.

theorem DirichletTransform.analyticOnNhd_carlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (carlsonRIntegral t b) carlsonRVariableDomain

The native unregularized R-integral is jointly analytic on the same variable domain.

theorem DirichletTransform.sum_mul_deriv_cpow_carlsonAffineForm {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : ∑ i : ι, z i * deriv (fun (w : ℂ) => carlsonAffineForm (Function.update z i w) u ^ t) (z i) = t * carlsonAffineForm z u ^ t

Euler's differential identity for the pointwise power kernel, corresponding to the second equation of Theorem 5.9-2.