Differentiating the quadratic transformations

The natural equal-parameter L-regularization is the exponent derivative of the equal-parameter R-regularization. In particular, its definition does not divide by the possibly vanishing quadraticGammaRatio.

Both quadratic identities are differentiated here, including the correction from the moving Dirichlet parameters. The parameter-transfer identity (1987), (2.12), identifies this correction with the transformed L-term, yielding (6.4) and (6.5). All complex exponent and Dirichlet parameters are allowed. The input node domains are those of the R-identities; transformed ratios use the slit-plane interface. At exponent zero the correction vanishes, giving both identities (6.8).

noncomputable def DirichletTransform.TwoVariable.regEqualLContinued (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (β : ℂ) : ℂ

The normalization by Γ(β + 1/2), retaining removable equal-parameter values.

Equations

• DirichletTransform.TwoVariable.regEqualLContinued t x y hz β = deriv (fun (s : ℂ) => DirichletTransform.TwoVariable.regEqualRContinued s x y hz β) t

theorem DirichletTransform.TwoVariable.hasDerivAt_regEqualRContinued_L (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => regEqualRContinued s x y hz β) (regEqualLContinued t x y hz β) t

theorem DirichletTransform.TwoVariable.analyticOnNhd_regEqualLContinued_joint (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (p : Fin 2 → ℂ) => regEqualLContinued (p 0) x y hz (p 1)) Set.univ

Entire dependence on both the exponent and the equal Dirichlet parameter.

theorem DirichletTransform.TwoVariable.analyticAt_regEqualLContinued_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f b : E → ℂ} {p : E} {x y : ℂ} (hz : pair x y ∈ carlsonRVariableDomain) (hf : AnalyticAt ℂ f p) (hb : AnalyticAt ℂ b p) : AnalyticAt ℂ (fun (w : E) => regEqualLContinued (f w) x y hz (b w)) p

Analytic substitutions in the exponent and equal parameter.

noncomputable def DirichletTransform.TwoVariable.equalLContinued (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (β : ℂ) : ℂ

The ordinary equal-parameter L-function. At genuine poles of Γ(β + 1/2) this is only a totalized expression; nonpositive integral β are removable values.

Equations

• DirichletTransform.TwoVariable.equalLContinued t x y hz β = Complex.Gamma (β + 1 / 2) * DirichletTransform.TwoVariable.regEqualLContinued t x y hz β

theorem DirichletTransform.TwoVariable.hasDerivAt_equalRContinued_L (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => equalRContinued s x y hz β) (equalLContinued t x y hz β) t

The ordinary equal-parameter L-function is the exponent derivative of ordinary R.

theorem DirichletTransform.TwoVariable.analyticAt_equalLContinued_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f b : E → ℂ} {p : E} {x y : ℂ} (hz : pair x y ∈ carlsonRVariableDomain) (hf : AnalyticAt ℂ f p) (hb : AnalyticAt ℂ b p) (hβ : IsCarlsonGammaRegular (b p + 1 / 2)) : AnalyticAt ℂ (fun (w : E) => equalLContinued (f w) x y hz (b w)) p

Holomorphy on Carlson's ordinary equal-parameter domain.

theorem DirichletTransform.TwoVariable.analyticAt_equalLContinued_neg_nat (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (n : ℕ) : AnalyticAt ℂ (equalLContinued t x y hz) (-↑n)

In particular, the nonpositive integral equal parameters are regular points, not poles of the ordinary L-continuation.

theorem DirichletTransform.TwoVariable.regEqualLContinued_eq_integral (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hβ : 0 < β.re) : regEqualLContinued t x y hz β = carlsonLIntegral t (pair β β) (pair x y) / Complex.Gamma (β + 1 / 2)

Agreement with the Gamma-normalized native L-integral on convergent parameters.

theorem DirichletTransform.TwoVariable.equalLContinued_eq_integral (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hβ : 0 < β.re) : equalLContinued t x y hz β = carlsonLIntegral t (pair β β) (pair x y)

Agreement of ordinary equal-parameter L with its convergent integral.

theorem DirichletTransform.TwoVariable.regCarlsonLContinued_pair_eq (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regCarlsonLContinued t (pair x y) hz (pair β β) = quadraticGammaRatio β * regEqualLContinued t x y hz β

Compatibility does not require cancelling the Gamma ratio.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_eq (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regCarlsonLSlit t (pair β β) (pair x y) = quadraticGammaRatio β * regEqualLContinued t x y hz β

Slit-interface compatibility on the node domain of the equal-parameter family.

noncomputable def DirichletTransform.TwoVariable.regRParameterTransfer (t u v x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : ℂ

The missing term when the exponent and the Dirichlet parameters both vary. The parameter sum u + v stays fixed along this derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.TwoVariable.regRParameterTransfer_eq_L (t u v x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regRParameterTransfer t u v x y hz = x ^ t * regCarlsonLSlit (-v) (pair (u + v + t) (-t)) (pair 1 (y / x))

Carlson (1987), (2.12), normalized at the first node. The ratio may lie outside the right half-plane, so the transformed L-function uses its slit continuation.

theorem DirichletTransform.TwoVariable.regRParameterTransfer_eq_neg_L (t u v x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regRParameterTransfer t u v x y hz = -(y ^ t * regCarlsonLSlit (-u) (pair (-t) (u + v + t)) (pair (x / y) 1))

Carlson (1987), second form of (2.12), normalized at the last node.

theorem DirichletTransform.TwoVariable.deriv_regRContinued_exponent_transfer (t u v x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : deriv (fun (s : ℂ) => regCarlsonRContinued s (pair x y) hz (pair (u + s) (v - s))) t = regCarlsonLContinued t (pair x y) hz (pair (u + t) (v - t)) + regRParameterTransfer t (u + t) (v - t) x y hz

Chain rule for the exponent and a sum-preserving parameter transfer.

theorem DirichletTransform.TwoVariable.regEqualLContinued_firstQuadratic_deriv (t β x y : ℂ) (hz : FirstQuadraticDomain x y) : 2 * regEqualLContinued (2 * t) x y ⋯ β = regCarlsonLContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (β + t) (1 / 2 - t)) + regRParameterTransfer t (β + t) (1 / 2 - t) (arithmeticMeanSq x y) (geometricMeanSq x y) ⋯

First quadratic identity with the full parameter-derivative correction.

theorem DirichletTransform.TwoVariable.regEqualLContinued_secondQuadratic_deriv (t β x y : ℂ) (hz : SecondQuadraticDomain x y) : regEqualLContinued t (x ^ 2) (y ^ 2) ⋯ β = regCarlsonLContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (2 * β + t) (1 / 2 - β - t)) + regRParameterTransfer t (2 * β + t) (1 / 2 - β - t) (arithmeticMeanSq x y) (geometricMeanSq x y) ⋯

Second quadratic identity with the full parameter-derivative correction.

theorem DirichletTransform.TwoVariable.regEqualLContinued_firstQuadratic (t β x y : ℂ) (hz : FirstQuadraticDomain x y) : 2 * regEqualLContinued (2 * t) x y ⋯ β = regCarlsonLSlit t (pair (β + t) (1 / 2 - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) - geometricMeanSq x y ^ t * regCarlsonLSlit (-(β + t)) (pair (-t) (β + 1 / 2 + t)) (pair (arithmeticMeanSq x y / geometricMeanSq x y) 1)

Carlson (1987), (6.4), for all complex parameters, retaining removable values. The second L-term is evaluated at the slit-plane ratio A / G.

theorem DirichletTransform.TwoVariable.regEqualLContinued_secondQuadratic (t β x y : ℂ) (hz : SecondQuadraticDomain x y) : regEqualLContinued t (x ^ 2) (y ^ 2) ⋯ β = regCarlsonLSlit t (pair (2 * β + t) (1 / 2 - β - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) - geometricMeanSq x y ^ t * regCarlsonLSlit (-(2 * β + t)) (pair (-t) (β + 1 / 2 + t)) (pair (arithmeticMeanSq x y / geometricMeanSq x y) 1)

Carlson (1987), (6.5) with the first forms of (6.6) and (6.7), for all complex parameters. No Gamma factor is cancelled in this normalization.

theorem DirichletTransform.TwoVariable.equalLContinued_firstQuadratic (t β x y : ℂ) (hz : FirstQuadraticDomain x y) : 2 * equalLContinued (2 * t) x y ⋯ β = carlsonLSlit t (pair (β + t) (1 / 2 - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) - geometricMeanSq x y ^ t * carlsonLSlit (-(β + t)) (pair (-t) (β + 1 / 2 + t)) (pair (arithmeticMeanSq x y / geometricMeanSq x y) 1)

The first quadratic transformation in ordinary normalization. Its finite-function interpretation uses Carlson's domain IsCarlsonGammaRegular (β + 1/2); the algebraic identity also holds for the totalized values at genuine poles.

theorem DirichletTransform.TwoVariable.equalLContinued_secondQuadratic (t β x y : ℂ) (hz : SecondQuadraticDomain x y) : equalLContinued t (x ^ 2) (y ^ 2) ⋯ β = carlsonLSlit t (pair (2 * β + t) (1 / 2 - β - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) - geometricMeanSq x y ^ t * carlsonLSlit (-(2 * β + t)) (pair (-t) (β + 1 / 2 + t)) (pair (arithmeticMeanSq x y / geometricMeanSq x y) 1)

The second quadratic transformation in ordinary normalization, with the same genuine-pole convention as equalLContinued_firstQuadratic.

@[simp]

theorem DirichletTransform.TwoVariable.regRParameterTransfer_zero (u v x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regRParameterTransfer 0 u v x y hz = 0

At degree zero a sum-preserving parameter derivative vanishes.

theorem DirichletTransform.TwoVariable.regEqualLContinued_firstQuadratic_zero (β x y : ℂ) (hz : FirstQuadraticDomain x y) : 2 * regEqualLContinued 0 x y ⋯ β = regCarlsonLContinued 0 (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair β (1 / 2))

Carlson (1987), first identity (6.8), with no Dirichlet parameter exclusions.

theorem DirichletTransform.TwoVariable.regEqualLContinued_secondQuadratic_zero (β x y : ℂ) (hz : SecondQuadraticDomain x y) : regEqualLContinued 0 (x ^ 2) (y ^ 2) ⋯ β = regCarlsonLContinued 0 (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (2 * β) (1 / 2 - β))

Carlson (1987), second identity (6.8), with no Dirichlet parameter exclusions.