Carlson's R-function: basic definitions

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

The native regularized integral representing R_t(b,z) / Γ(∑ i, b i).

Equations

• DirichletTransform.regCarlsonRIntegral t b z = DirichletTransform.regCarlsonDirichletAverage b z fun (w : ℂ) => w ^ t

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

Carlson's native, unregularized R_t integral.

Equations

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

theorem DirichletTransform.carlsonRIntegral_eq_Gamma_mul_reg {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) : carlsonRIntegral t b z = Complex.Gamma (∑ i : ι, b i) * regCarlsonRIntegral t b z

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

def DirichletTransform.carlsonRVariableDomain {ι : Type u_1} : Set (ι → ℂ)

The branch-safe domain where every Carlson variable lies in the open right half-plane.

Equations

• DirichletTransform.carlsonRVariableDomain = {z : ι → ℂ | ∀ (i : ι), z i ∈ DirichletTransform.carlsonRightHalfPlane}

theorem DirichletTransform.isOpen_carlsonRVariableDomain {ι : Type u_1} [Finite ι] : IsOpen carlsonRVariableDomain

Carlson's right-half-plane variable domain is open.

theorem DirichletTransform.carlsonAffineForm_mem_rightHalfPlane {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : carlsonAffineForm z u ∈ carlsonRightHalfPlane

A convex combination of points in the right half-plane remains there.

theorem DirichletTransform.carlsonRightHalfPlane_subset_slitPlane : carlsonRightHalfPlane ⊆ Complex.slitPlane

The right half-plane is contained in Mathlib's principal-branch slit plane.

theorem DirichletTransform.carlsonAffineForm_mem_slitPlane {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : carlsonAffineForm z u ∈ Complex.slitPlane

On the Carlson variable domain, the affine kernel lies in the principal-branch slit plane.