Carlson's L-function on the full product slit plane

The exponent derivative of regCarlsonRSlit is jointly holomorphic in the exponent, Dirichlet parameters, and slit-plane nodes. This completes the domain assertion of Carlson (1987), (2.1), in regularized form. The original right-half-plane continuation is retained and agrees with this extension. No equality with a principal-power simplex integral is asserted for arbitrary slit-plane nodes.

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

The entire regularized L-function, defined by differentiating R in its exponent. Values outside the product slit plane are unspecified.

Equations

• DirichletTransform.regCarlsonLSlit t b z = deriv (fun (s : ℂ) => DirichletTransform.regCarlsonRSlit s b z) t

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

The ordinary L-function on slit-plane nodes. At total-parameter Gamma poles, this is only Lean's totalized expression, not a claimed finite value.

Equations

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

theorem DirichletTransform.hasDerivAt_regCarlsonRSlit_L {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : HasDerivAt (fun (s : ℂ) => regCarlsonRSlit s b z) (regCarlsonLSlit t b z) t

theorem DirichletTransform.analyticOnNhd_regCarlsonLSlit_joint {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => regCarlsonLSlit (p none) (fun (i : ι) => p (some (Sum.inl i))) fun (i : ι) => p (some (Sum.inr i))) {p : Option (ι ⊕ ι) → ℂ | (fun (i : ι) => p (some (Sum.inr i))) ∈ carlsonRSlitDomain}

Carlson (1987), (2.1): full joint holomorphy, with no parameter exceptions after Gamma regularization. The coordinates are exponent, parameters, then nodes.

theorem DirichletTransform.analyticAt_regCarlsonLSlit_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {t : E → ℂ} {b z : E → ι → ℂ} {p : E} (ht : AnalyticAt ℂ t p) (hb : AnalyticAt ℂ b p) (hz : AnalyticAt ℂ z p) (hslit : z p ∈ carlsonRSlitDomain) : AnalyticAt ℂ (fun (q : E) => regCarlsonLSlit (t q) (b q) (z q)) p

Analytic substitutions in all arguments preserve analyticity on the slit domain.

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

theorem DirichletTransform.analyticOnNhd_regCarlsonLSlit_exponent_parameters {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : AnalyticOnNhd ℂ (fun (p : Option ι → ℂ) => regCarlsonLSlit (p none) (fun (i : ι) => p (some i)) z) Set.univ

theorem DirichletTransform.analyticAt_carlsonLSlit_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {t : E → ℂ} {b z : E → ι → ℂ} {p : E} (ht : AnalyticAt ℂ t p) (hb : AnalyticAt ℂ b p) (hz : AnalyticAt ℂ z p) (hslit : z p ∈ carlsonRSlitDomain) (hc : ∀ (n : ℕ), ∑ i : ι, b p i ≠ -↑n) : AnalyticAt ℂ (fun (q : E) => carlsonLSlit (t q) (b q) (z q)) p

theorem DirichletTransform.regCarlsonLSlit_eq_continued {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonLSlit t b z = regCarlsonLContinued t z hz b

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

theorem DirichletTransform.carlsonLSlit_eq_continued {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : carlsonLSlit t b z = carlsonLContinued t z hz b

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

theorem DirichletTransform.eqOn_regCarlsonLSlit_of_eq_continued {ι : Type u_1} [Fintype ι] {t : ℂ} {b : ι → ℂ} {F : (ι → ℂ) → ℂ} (hF : AnalyticOnNhd ℂ F carlsonRSlitDomain) (heq : ∀ (z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain), F z = regCarlsonLContinued t z hz b) : Set.EqOn F (regCarlsonLSlit t b) carlsonRSlitDomain

The continuation is uniquely determined by its right-half-plane values.

theorem DirichletTransform.hasDerivAt_carlsonRSlit_L {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : HasDerivAt (fun (s : ℂ) => carlsonRSlit s b z) (carlsonLSlit t b z) t

Differentiating the ordinary R-function gives the ordinary L-function.

@[simp]

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