Slit-plane domains for Carlson's R-function

The product slit plane is star-convex about the constant node vector 1. The segment from 1 to each node stays on the principal branch, as required by the single-integral construction in Carlson's Section 6.8. Arbitrary convex combinations of nodes need not stay on this branch; the original simplex integral is therefore not used on this domain.

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

The full principal-branch node domain for Carlson's R-function.

Equations

• DirichletTransform.carlsonRSlitDomain = {z : ι → ℂ | ∀ (i : ι), z i ∈ Complex.slitPlane}

theorem DirichletTransform.carlsonRVariableDomain_subset_slitDomain {ι : Type u_1} : carlsonRVariableDomain ⊆ carlsonRSlitDomain

theorem DirichletTransform.isOpen_carlsonRSlitDomain {ι : Type u_1} [Finite ι] : IsOpen carlsonRSlitDomain

theorem DirichletTransform.one_mem_carlsonRSlitDomain {ι : Type u_1} : (fun (x : ι) => 1) ∈ carlsonRSlitDomain

theorem DirichletTransform.starConvex_one_carlsonRSlitDomain {ι : Type u_1} : StarConvex ℝ (fun (x : ι) => 1) carlsonRSlitDomain

theorem DirichletTransform.isPreconnected_carlsonRSlitDomain {ι : Type u_1} : IsPreconnected carlsonRSlitDomain

theorem DirichletTransform.carlsonRSegment_mem_slitPlane {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (i : ι) : 1 - ↑u + ↑u * z i ∈ Complex.slitPlane

Each factor of the single-integral kernel avoids the branch cut on the closed interval.

theorem DirichletTransform.carlsonRSlitDomain_inv {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : (fun (i : ι) => (z i)⁻¹) ∈ carlsonRSlitDomain

Taking coordinatewise reciprocals preserves the full principal-branch node domain.