Native power-logarithm averages on the slit plane #
The slit L-function is the domain-aware continuation of w ^ t * log w.
Native-integral agreement and the exponent-derivative relation now hold whenever
the entire node convex hull lies in the slit plane. Merely asking that each node
avoid the cut would be insufficient. All statements allow empty index types.
theorem
DirichletTransform.isJointRegCarlsonContinuationOn_regCarlsonLSlit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
:
IsJointRegCarlsonContinuationOn Complex.slitPlane (carlsonLKernel t) fun (p : (ι → ℂ) × (ι → ℂ)) =>
regCarlsonLSlit t p.1 p.2
The slit L-function is the domain-aware continuation of the power-logarithm kernel.
theorem
DirichletTransform.isRegCarlsonContinuation_regCarlsonLSlit_of_convexHull
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
{z : ι → ℂ}
(hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane)
:
IsRegCarlsonContinuation (carlsonLKernel t) z fun (b : ι → ℂ) => regCarlsonLSlit t b z
Entire-parameter characterization at every native-admissible slit tuple.
theorem
DirichletTransform.regCarlsonLSlit_eq_integral_of_convexHull
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
{b z : ι → ℂ}
(hb : b ∈ Complex.mvBetaConvergent)
(hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane)
:
Native L-integral agreement wherever the whole node convex hull avoids the cut.
theorem
DirichletTransform.carlsonLSlit_eq_integral_of_convexHull
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
{b z : ι → ℂ}
(hb : b ∈ Complex.mvBetaConvergent)
(hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane)
:
Native agreement with the ordinary L-normalization.
theorem
DirichletTransform.hasDerivAt_regCarlsonRIntegral_L_of_convexHull
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
{b z : ι → ℂ}
(hb : b ∈ Complex.mvBetaConvergent)
(hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane)
:
HasDerivAt (fun (s : ℂ) => regCarlsonRIntegral s b z) (regCarlsonLIntegral t b z) t
Differentiating the native R-integral inserts the logarithm on the full convex-hull-admissible node domain, with no right-half-plane restriction.