Equal-parameter continuation and quadratic transformations

The equal-parameter family R_t(β, β; x, y) has a larger parameter domain than one obtains by excluding all poles of Γ(2β): the values at nonpositive integer β are removable. Its natural regularization divides by Γ(β + 1/2).

We construct that entire regularization uniquely by agreement with the native integral on re β > 0. Square roots in the positive component allow the second quadratic identity to supply existence for any right-half-plane nodes. Both quadratic transformations then identify this canonical continuation, including its removable values. The ordinary function is analytic wherever β + 1/2 is not a nonpositive integer. No extension of the node domains is asserted here.

def DirichletTransform.TwoVariable.IsRegEqualRContinuation (t x y : ℂ) (G : ℂ → ℂ) : Prop

Characterization of the entire equal-parameter regularization.

Equations

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

theorem DirichletTransform.TwoVariable.IsRegEqualRContinuation.unique {t x y : ℂ} {F G : ℂ → ℂ} (hF : IsRegEqualRContinuation t x y F) (hG : IsRegEqualRContinuation t x y G) : F = G

Native agreement uniquely determines the entire equal-parameter regularization.

theorem DirichletTransform.TwoVariable.isRegEqualRContinuation_firstQuadratic (t x y : ℂ) (hz : FirstQuadraticDomain x y) : IsRegEqualRContinuation (2 * t) x y fun (β : ℂ) => regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (β + t) (1 / 2 - t))

The first transformed regularized function gives the entire equal-parameter family.

theorem DirichletTransform.TwoVariable.isRegEqualRContinuation_secondQuadratic (t x y : ℂ) (hz : SecondQuadraticDomain x y) : IsRegEqualRContinuation t (x ^ 2) (y ^ 2) fun (β : ℂ) => regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (2 * β + t) (1 / 2 - β - t))

The second transformed regularized function gives the entire equal-parameter family.

theorem DirichletTransform.TwoVariable.exists_isRegEqualRContinuation (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : ∃ (G : ℂ → ℂ), IsRegEqualRContinuation t x y G

Existence on arbitrary right-half-plane nodes, without selecting a square-root branch in the definition of the continuation.

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

Canonical entire continuation of R_t(β, β; x, y) / Γ(β + 1/2).

Equations

• DirichletTransform.TwoVariable.regEqualRContinued t x y hz = ⋯.choose

theorem DirichletTransform.TwoVariable.isRegEqualRContinuation_regEqualRContinued (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : IsRegEqualRContinuation t x y (regEqualRContinued t x y hz)

The chosen continuation satisfies the native characterization.

theorem DirichletTransform.TwoVariable.analyticOnNhd_regEqualRContinued (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (regEqualRContinued t x y hz) Set.univ

The canonical equal-parameter regularization is entire in β.

theorem DirichletTransform.TwoVariable.regEqualRContinued_firstQuadratic (t β x y : ℂ) (hz : FirstQuadraticDomain x y) : regEqualRContinued (2 * t) x y ⋯ β = regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (β + t) (1 / 2 - t))

First quadratic transformation with the natural equal-parameter regularization. Unlike the general Γ(2β) regularization, this loses no information at integral β.

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

Second quadratic transformation with the natural equal-parameter regularization.

theorem DirichletTransform.TwoVariable.regCarlsonRContinued_pair_eq (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regCarlsonRContinued t (pair x y) hz (pair β β) = quadraticGammaRatio β * regEqualRContinued t x y hz β

Compatibility with the general regularized R-function. The factor can vanish; the equal-parameter regularization retains the removable values in that case.

theorem DirichletTransform.TwoVariable.analyticAt_regEqualRContinued_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) => regEqualRContinued (f w) x y hz (b w)) p

Joint analytic dependence on the exponent and the equal Dirichlet parameter.

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

Equal-parameter ordinary R. At genuine poles of Γ(β + 1/2) this definition is totalized; analyticity and its interpretation as continuation are asserted on the Gamma-regular domain, which includes every nonpositive integer β.

Equations

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

theorem DirichletTransform.TwoVariable.equalRContinued_eq_integral (t β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hβ : 0 < β.re) : equalRContinued t x y hz β = rIntegral t β β x y

Agreement with the original integral wherever that integral converges.

theorem DirichletTransform.TwoVariable.analyticOnNhd_equalRContinued (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (equalRContinued t x y hz) {β : ℂ | IsCarlsonGammaRegular (β + 1 / 2)}

Analyticity of the ordinary equal-parameter function on Carlson's parameter domain.

theorem DirichletTransform.TwoVariable.isCarlsonGammaRegular_neg_nat_add_half (n : ℕ) : IsCarlsonGammaRegular (-↑n + 1 / 2)

The nonpositive integral parameters are in the ordinary continuation domain.

@[simp]

theorem DirichletTransform.TwoVariable.regEqualRContinued_zero (β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : regEqualRContinued 0 x y hz β = (Complex.Gamma (β + 1 / 2))⁻¹

At exponent zero the entire equal-parameter regularization is reciprocal Gamma.

@[simp]

theorem DirichletTransform.TwoVariable.equalRContinued_zero (β x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hβ : IsCarlsonGammaRegular (β + 2⁻¹)) : equalRContinued 0 x y hz β = 1

Regression check for the removable values: the exponent-zero function is one, including at β = 0, -1, -2, ....

theorem DirichletTransform.TwoVariable.equalRContinued_firstQuadratic (t β x y : ℂ) (hz : FirstQuadraticDomain x y) (_hβ : IsCarlsonGammaRegular (β + 1 / 2)) : equalRContinued (2 * t) x y ⋯ β = Complex.Gamma (β + 1 / 2) * regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (β + t) (1 / 2 - t))

Carlson 6.9-3 on the full common parameter domain of the ordinary functions.

theorem DirichletTransform.TwoVariable.equalRContinued_secondQuadratic (t β x y : ℂ) (hz : SecondQuadraticDomain x y) (_hβ : IsCarlsonGammaRegular (β + 1 / 2)) : equalRContinued t (x ^ 2) (y ^ 2) ⋯ β = Complex.Gamma (β + 1 / 2) * regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (2 * β + t) (1 / 2 - β - t))

Carlson 6.10-1 on the full common parameter domain of the ordinary functions.