Documentation

LeanPool.CarlsonFunctions.Carlson.TwoVariable.T

The two-variable Carlson T-function #

This file specializes the multivariate T-function of Carlson's Definition 5.12-1 to two variables. Later files may develop Carlson's singular limit in which one variable tends to zero; special-function identifications do not belong here.

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

The canonical two-variable specialization of the native regularized T-integral.

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

    The canonical two-variable specialization of Carlson's native T-integral.

    Equations
    Instances For
      source
      def DirichletTransform.TwoVariable.TVariableDomain (x y : ℂ) :
      Prop

      The intrinsic domain for the two-variable T-integral.

      Equations
      Instances For
        source
        theorem DirichletTransform.TwoVariable.affine_pair_ne_zero_of_mem_TVariableDomain {x y : ℂ} (hxy : TVariableDomain x y) {u : Fin 2 → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ (Fin 2)) :
        carlsonAffineForm (pair x y) u ≠ 0

        On the two-variable T-domain, every affine combination occurring in the Euler-simplex integral is nonzero.

        source
        theorem DirichletTransform.TwoVariable.integrableOn_regDirichletDensity_mul_TKernel {b₀ b₁ x y : ℂ} (hb : pair b₀ b₁ ∈ Complex.mvBetaConvergent) (hxy : TVariableDomain x y) :
        MeasureTheory.IntegrableOn (fun (u : Fin 2 → ℝ) => ProbabilityTheory.regDirichletDensity (pair b₀ b₁) u * carlsonTKernel (carlsonAffineForm (pair x y) u)) (Convexity.StdSimplex.coordinateSet ℝ (Fin 2)) MeasureTheory.Measure.stdSimplexMeasure

        The two-variable T-integrand is integrable on its native parameter and variable domain.

        source
        theorem DirichletTransform.TwoVariable.regTIntegral_swap (b₀ b₁ x y : ℂ) :
        regTIntegral b₁ b₀ y x = regTIntegral b₀ b₁ x y

        Simultaneously exchanging the parameters and variables leaves the regularized two-variable T-integral unchanged.

        source
        def DirichletTransform.TwoVariable.IsRegTContinuation (x y : ℂ) (G : (Fin 2 → ℂ) → ℂ) :
        Prop

        A two-variable T-continuation is the multivariate continuation specialized to a pair of variables.

        Equations
        Instances For
          source
          theorem DirichletTransform.TwoVariable.IsRegTContinuation.analyticOnNhd {x y : ℂ} {G : (Fin 2 → ℂ) → ℂ} (hG : IsRegTContinuation x y G) :
          AnalyticOnNhd ℂ G Set.univ

          A two-variable regularized T-continuation is entire in its two Dirichlet parameters.

          source
          theorem DirichletTransform.TwoVariable.exists_isRegTContinuation {x y : ℂ} (hxy : TVariableDomain x y) :
          ∃ (G : (Fin 2 → ℂ) → ℂ), IsRegTContinuation x y G

          On the intrinsic variable domain, an entire regularized two-variable T-continuation exists.

          source
          theorem DirichletTransform.TwoVariable.IsRegTContinuation.eq {x y : ℂ} {G H : (Fin 2 → ℂ) → ℂ} (hG : IsRegTContinuation x y G) (hH : IsRegTContinuation x y H) :
          G = H

          The entire regularized two-variable T-continuation is unique.