The two-variable Carlson S-function

theorem DirichletTransform.TwoVariable.regSSeries_eq_regSIntegral (b₀ b₁ z₀ z₁ : ℂ) (hb : pair b₀ b₁ ∈ Complex.mvBetaConvergent) : regSSeries b₀ b₁ z₀ z₁ = regSIntegral b₀ b₁ z₀ z₁

On the native convergence region, the two-variable S-series agrees with its Dirichlet integral.

theorem DirichletTransform.TwoVariable.regSIntegral_swap (b₀ b₁ z₀ z₁ : ℂ) : regSIntegral b₁ b₀ z₁ z₀ = regSIntegral b₀ b₁ z₀ z₁

Simultaneously exchanging the two parameters and variables leaves the native regularized S-integral unchanged.

theorem DirichletTransform.TwoVariable.regSSeries_add_const (b₀ b₁ z₀ z₁ a : ℂ) : regSSeries b₀ b₁ (z₀ + a) (z₁ + a) = Complex.exp a * regSSeries b₀ b₁ z₀ z₁

Translating both variables gives the global exponential translation formula for the analytically continued two-variable S-series.

theorem DirichletTransform.TwoVariable.tendsto_regRIntegral_confluent (b₀ b₁ z₀ z₁ : ℂ) (hb : pair b₀ b₁ ∈ Complex.mvBetaConvergent) : Filter.Tendsto (fun (n : ℕ) => regRIntegral (↑n) b₀ b₁ (1 + z₀ / ↑n) (1 + z₁ / ↑n)) Filter.atTop (nhds (regSIntegral b₀ b₁ z₀ z₁))

The natural-power two-variable R-integrals coalesce to the two-variable S-integral.