Continuation of Carlson's R-function in the nodes

For every complex exponent and every complex Dirichlet parameter vector, the regularized R-function has a unique holomorphic extension to the product slit plane. The construction starts with Carlson's beta-weighted single integral (Theorem 6.8-1). Two division-free associated relations move any parameters into its convergence strip. In particular, no exceptional parameter hyperplanes are removed by this construction.

Uniqueness is on the slit domain, not on the arbitrary values of a total Lean function outside that domain. This file does not assert the contour representation (6.8-7).

def DirichletTransform.IsCarlsonRSlitContinuation {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) (F : (ι → ℂ) → ℂ) : Prop

A holomorphic extension in the nodes of the existing parameter continuation.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.eqOn_carlsonRSlitDomain_of_eqOn_rightHalfPlane {ι : Type u_1} [Fintype ι] {F G : (ι → ℂ) → ℂ} (hF : AnalyticOnNhd ℂ F carlsonRSlitDomain) (hG : AnalyticOnNhd ℂ G carlsonRSlitDomain) (hFG : Set.EqOn F G carlsonRVariableDomain) : Set.EqOn F G carlsonRSlitDomain

Agreement on the right half-plane determines a holomorphic function on the product slit plane uniquely. This is the node-variable permanence principle.

theorem DirichletTransform.IsCarlsonRSlitContinuation.eqOn {ι : Type u_1} [Fintype ι] {t : ℂ} {b : ι → ℂ} {F G : (ι → ℂ) → ℂ} (hF : IsCarlsonRSlitContinuation t b F) (hG : IsCarlsonRSlitContinuation t b G) : Set.EqOn F G carlsonRSlitDomain

theorem DirichletTransform.exists_carlsonRSlitContinuation {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) : ∃ (F : (ι → ℂ) → ℂ), IsCarlsonRSlitContinuation t b F

Every complex exponent and parameter vector admits a holomorphic extension in the nodes. The proof works for empty index types as well: the associated sums are then empty.

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

The regularized Carlson function on the full product slit plane, for arbitrary complex t and b. Values outside carlsonRSlitDomain are unspecified.

Equations

• DirichletTransform.regCarlsonRSlit t b z = ⋯.choose z

theorem DirichletTransform.isCarlsonRSlitContinuation_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) : IsCarlsonRSlitContinuation t b (regCarlsonRSlit t b)

theorem DirichletTransform.analyticOnNhd_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) : AnalyticOnNhd ℂ (regCarlsonRSlit t b) carlsonRSlitDomain

theorem DirichletTransform.regCarlsonRSlit_eq_continued {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRSlit t b z = regCarlsonRContinued t z hz b

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

The ordinary Carlson function on the slit domain, away from poles of the total-parameter Gamma factor. At those poles this definition is only Lean's totalized expression.

Equations

• DirichletTransform.carlsonRSlit t b z = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonRSlit t b z

theorem DirichletTransform.analyticOnNhd_carlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) : AnalyticOnNhd ℂ (carlsonRSlit t b) carlsonRSlitDomain

theorem DirichletTransform.regCarlsonRSlit_eq_integral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonRSlit t b z = regCarlsonRIntegral t b z

The slit continuation agrees with the native simplex integral wherever the latter was already used to define Carlson's principal branch.

theorem DirichletTransform.carlsonRSlit_eq_integral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : carlsonRSlit t b z = carlsonRIntegral t b z

theorem DirichletTransform.carlsonRUnitIntervalIntegral_eq_gamma_mul_slit {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hz : z ∈ carlsonRSlitDomain) : carlsonRUnitIntervalIntegral a a' b z = Complex.Gamma a * Complex.Gamma a' * regCarlsonRSlit (-a) b z

Carlson's single-integral representation now holds on the full product slit plane.

theorem DirichletTransform.regCarlsonRSlit_eq_sum_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : regCarlsonRSlit t b z = ∑ i : ι, b i * regCarlsonRSlit t (addDirichletUnit b i) z

The first associated relation on the full node domain, without parameter exceptions.

theorem DirichletTransform.regCarlsonRSlit_add_one_eq_sum_mul_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : regCarlsonRSlit (t + 1) b z = ∑ i : ι, b i * z i * regCarlsonRSlit t (addDirichletUnit b i) z

The second associated relation on the full node domain, without parameter exceptions.

theorem DirichletTransform.regCarlsonRSlit_eq_zero_of_isEmpty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : regCarlsonRSlit t b z = 0

The empty-index convention is preserved by the node continuation.