Documentation

LeanPool.CarlsonFunctions.Carlson.TwoVariable.L

Two-variable L-functions and elementary logarithmic values #

The two-variable interface parallels TwoVariable.R. The exceptional elementary case L_{-1}(1,1;x,y) is Carlson (1987), (8.8). Its undivided identity includes coincident nodes; the diagonal value is supplied separately.

source
@[reducible, inline]
noncomputable abbrev DirichletTransform.TwoVariable.regLIntegral (t b₀ b₁ x y : ℂ) :
ℂ

The two-variable native regularized L-integral.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev DirichletTransform.TwoVariable.lIntegral (t b₀ b₁ x y : ℂ) :
    ℂ

    The two-variable native normalized L-integral.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev DirichletTransform.TwoVariable.regLContinued (t b₀ b₁ x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) :
      ℂ

      The two-variable entire regularized L-continuation.

      Equations
      Instances For
        source
        theorem DirichletTransform.TwoVariable.regLIntegral_swap (t b₀ b₁ x y : ℂ) :
        regLIntegral t b₀ b₁ x y = regLIntegral t b₁ b₀ y x

        Symmetry exchanges the two parameters together with their nodes.

        source
        theorem DirichletTransform.TwoVariable.sub_mul_regAverage_deriv {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f carlsonRightHalfPlane) (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) :
        (x - y) * regCarlsonDirichletAverage (pair 1 1) (pair x y) (deriv f) = f x - f y

        The fundamental theorem for the uniform two-node Dirichlet average.

        source
        theorem DirichletTransform.TwoVariable.sub_mul_regLContinued_neg_one_one_one (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) :
        (x - y) * regLContinued (-1) 1 1 x y hz = (Complex.log x ^ 2 - Complex.log y ^ 2) / 2

        Equation (8.8), without division by the node difference.

        source
        theorem DirichletTransform.TwoVariable.regLContinued_neg_one_one_one (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hxy : x ≠ y) :
        regLContinued (-1) 1 1 x y hz = (Complex.log x ^ 2 - Complex.log y ^ 2) / (2 * (x - y))

        The elementary divided-logarithm formula of Carlson (1987), (8.8).

        source
        theorem DirichletTransform.TwoVariable.regLContinued_neg_one_one_one_diag (x : ℂ) (hz : pair x x ∈ carlsonRVariableDomain) :
        regLContinued (-1) 1 1 x x hz = x⁻¹ * Complex.log x

        The diagonal value completes the exceptional elementary formula.

        source
        theorem DirichletTransform.TwoVariable.sub_mul_regLContinued_one_one (t x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) :
        (x - y) * ((t + 1) * regLContinued t 1 1 x y hz + regCarlsonRContinued t (pair x y) hz (pair 1 1)) = x ^ (t + 1) * Complex.log x - y ^ (t + 1) * Complex.log y

        The uniform two-node reduction underlying (8.5), stated without division. At t = -1 it reduces to the logarithmic R-identity, so the separate formula regLContinued_neg_one_one_one is needed to evaluate L there.

        source
        theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_contiguous (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) :
        u * (y - x) * regCarlsonLSlit t (pair (u + 1) v) (pair x y) = y * regCarlsonLSlit t (pair u v) (pair x y) - regCarlsonLSlit (t + 1) (pair u v) (pair x y)

        Carlson (1987), (3.9), in a division-free regularized form. The identity is valid at coincident nodes and at every complex Dirichlet parameter.