Native-integral agreement on the slit plane

Carlson's slit continuation agrees with its principal-power simplex integral whenever the entire node convex hull avoids the branch cut, not only when all nodes lie in the right half-plane. This identifies regCarlsonRSlit with the domain-aware continuation of the power kernel and connects it to the continued circle-Cauchy representation.

Nodewise membership in the slit plane alone is not enough for native integral agreement: the convex hull may meet the cut. The general simply connected continuation theorem for arbitrary scalar kernels is still separate work.

theorem DirichletTransform.isJointRegCarlsonContinuationOn_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) : IsJointRegCarlsonContinuationOn Complex.slitPlane (fun (w : ℂ) => w ^ t) fun (p : (ι → ℂ) × (ι → ℂ)) => regCarlsonRSlit t p.1 p.2

The slit R-function satisfies the general-average characterization, with native agreement wherever the full node convex hull lies in the slit plane.

theorem DirichletTransform.isRegCarlsonRContinuation_regCarlsonRSlit_of_convexHull {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane) : IsRegCarlsonRContinuation t z fun (b : ι → ℂ) => regCarlsonRSlit t b z

The entire-parameter R-continuation is characterized by its native integral on every convex-hull-admissible slit tuple.

theorem DirichletTransform.regCarlsonRSlit_eq_integral_of_convexHull {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane) : regCarlsonRSlit t b z = regCarlsonRIntegral t b z

Principal-branch native agreement on the full admissible convex-hull domain.

theorem DirichletTransform.carlsonRSlit_eq_integral_of_convexHull {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane) : carlsonRSlit t b z = carlsonRIntegral t b z

The same native agreement with the ordinary normalization.

theorem DirichletTransform.regCarlsonRSlit_eq_circleIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hD : Metric.closedBall c R ⊆ Complex.slitPlane) (hz : Set.range z ⊆ Metric.ball c R) : regCarlsonRSlit t b z = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), continuedRegCarlsonResolvent 0 b z s * s ^ t

The circle form of the generalized Cauchy representation for R_t, at all complex parameters. This is the power-kernel specialization of 6.3-4, not the different beta-resolvent ellipse formula 6.8-7.