{"id":"palomar/PALOMAR-2026-09-15-000004","url":"https://github.com/bjbraams/lean-codes/tree/b7ed9a789ef8f1dea50cf82e29b7aded2b07b097","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000004-v1.json","repo":"https://github.com/bjbraams/lean-codes","tags":["math.CA","math.CV","msc:33C65","msc:32A05","special-functions","complex-analysis","lean-formalization"],"score":0,"title":"B. C. Carlson's approach to special functions of applied mathematics","trust":"high","domain":"math.CA","source":"palomar","authors":["Bastiaan J Braams"],"reviews":0,"subject":"math.CA","summary":"Lean formalization of selected results in B. C. Carlson's theory of special functions as complex Dirichlet averages. The registry selection establishes joint entire-parameter continuation of holomorphic averages on convex open scalar domains; joint holomorphy and native-integral agreement for the Gamma-regularized R and L functions on principal slit-node domains; Euler inversion and Euler-Poisson equations; and Gamma-regularized adaptations of both quadratic R transformations for all complex exponent and Dirichlet parameters with positive-real-part unsquared variables. The L function is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"Special Functions of Applied Mathematics","identifier":"Academic Press, 1977","relationship":"formalizes"},{"title":"Special Functions of Applied Mathematics","identifier":"Academic Press, 1977","relationship":"adapts"},{"title":"Dirichlet averages of x^t log x","identifier":"SIAM Journal on Mathematical Analysis 18 (1987), 550–565","relationship":"formalizes"},{"title":"Lecture notes on several complex variables","identifier":"Lecture notes, 2013","relationship":"adapts"},{"title":"Continuous Multivariate Distributions, Volume 1: Models and Applications","identifier":"Wiley, 2000; DOI 10.1002/0471722065","relationship":"formalizes"}]}