Documentation

LeanPool.CarlsonFunctions.Carlson.R.Laplace

The Laplace representation of Carlson's R-function #

This file develops the inverse confluence formula of [Carl77, Theorem 5.10-2], which expresses R as a one-dimensional Laplace--Mellin transform of S.

References #

source
noncomputable def DirichletTransform.regCarlsonRLaplaceIntegral {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) :
ℂ

The regularized Laplace--Mellin expression in Carlson's inverse confluence formula.

Equations
Instances For
    source
    noncomputable def DirichletTransform.carlsonRLaplaceIntegral {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) :
    ℂ

    The unregularized Laplace--Mellin expression in Carlson's inverse confluence formula.

    Equations
    Instances For
      source
      theorem DirichletTransform.carlsonRLaplaceIntegral_eq_Gamma_mul_reg {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) :
      carlsonRLaplaceIntegral a b z = Complex.Gamma (∑ i : ι, b i) * regCarlsonRLaplaceIntegral a b z

      Regularization in the Dirichlet parameters commutes with Carlson's one-dimensional Laplace--Mellin construction.

      source
      theorem DirichletTransform.integral_carlsonLaplaceKernel_ofReal {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
      ∫ (y : ℝ) in Set.Ioi 0, ↑y ^ (a - 1) * Complex.exp (-(↑r * ↑y)) = (1 / ↑r) ^ a * Complex.Gamma a

      The scalar Gamma integral underlying Carlson's inverse confluence formula, for a positive real decay rate.

      source
      theorem DirichletTransform.norm_carlsonLaplaceKernel {a w : ℂ} {y : ℝ} (hy : 0 < y) :
      ‖↑y ^ (a - 1) * Complex.exp (-↑y * w)‖ = Real.exp (-w.re * y) * y ^ (a.re - 1)

      Pointwise norm of the complex-rate Gamma kernel.

      source
      theorem DirichletTransform.integrableOn_carlsonLaplaceKernel_ofReal {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
      MeasureTheory.IntegrableOn (fun (y : ℝ) => ↑y ^ (a - 1) * Complex.exp (-(↑r * ↑y))) (Set.Ioi 0) MeasureTheory.volume

      The integrand of integral_carlsonLaplaceKernel_ofReal is integrable.

      source
      theorem DirichletTransform.continuousOn_carlsonLaplaceKernel (a w : ℂ) :
      ContinuousOn (fun (y : ℝ) => ↑y ^ (a - 1) * Complex.exp (-↑y * w)) (Set.Ioi 0)

      Continuity of the complex-rate Gamma kernel on (0, ∞).

      source
      theorem DirichletTransform.integrableOn_carlsonLaplaceKernel {a w : ℂ} (ha : 0 < a.re) (hw : 0 < w.re) :
      MeasureTheory.IntegrableOn (fun (y : ℝ) => ↑y ^ (a - 1) * Complex.exp (-↑y * w)) (Set.Ioi 0) MeasureTheory.volume

      Integrability of the complex-rate Gamma kernel on (0, ∞).

      source
      theorem DirichletTransform.hasDerivAt_integral_carlsonLaplaceKernel {a w : ℂ} (ha : 0 < a.re) (hw : 0 < w.re) :
      HasDerivAt (fun (w' : ℂ) => ∫ (y : ℝ) in Set.Ioi 0, ↑y ^ (a - 1) * Complex.exp (-↑y * w')) (∫ (y : ℝ) in Set.Ioi 0, -(↑y * (↑y ^ (a - 1) * Complex.exp (-↑y * w)))) w

      The Laplace kernel is holomorphic in the decay rate throughout the right half-plane.

      source
      theorem DirichletTransform.integral_carlsonLaplaceKernel {a w : ℂ} (ha : 0 < a.re) (hw : 0 < w.re) :
      ∫ (y : ℝ) in Set.Ioi 0, ↑y ^ (a - 1) * Complex.exp (-↑y * w) = w ^ (-a) * Complex.Gamma a

      The complex-rate Gamma integral needed in Carlson's inverse confluence theorem.

      source
      theorem DirichletTransform.regCarlsonRIntegral_eq_regCarlsonRLaplaceIntegral {ι : Type u_1} [Fintype ι] {a : ℂ} (ha : 0 < a.re) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) :
      regCarlsonRIntegral (-a) b z = regCarlsonRLaplaceIntegral a b z

      Carlson's inverse confluence formula, Theorem 5.10-2, in regularized form.

      source
      theorem DirichletTransform.carlsonRIntegral_eq_carlsonRLaplaceIntegral {ι : Type u_1} [Fintype ι] {a : ℂ} (ha : 0 < a.re) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) :
      carlsonRIntegral (-a) b z = carlsonRLaplaceIntegral a b z

      Carlson's inverse confluence formula in the native unregularized normalization.