The two-variable Carlson R-function

theorem DirichletTransform.TwoVariable.regRIntegral_natCast (n : ℕ) (b₀ b₁ z₀ z₁ : ℂ) (hb : pair b₀ b₁ ∈ Complex.mvBetaConvergent) : regRIntegral (↑n) b₀ b₁ z₀ z₁ = regRPolynomial n b₀ b₁ z₀ z₁

The two-variable integral at a natural exponent agrees with the Carlson polynomial.

theorem DirichletTransform.TwoVariable.regRIntegral_swap (t b₀ b₁ z₀ z₁ : ℂ) : regRIntegral t b₁ b₀ z₁ z₀ = regRIntegral t b₀ b₁ z₀ z₁

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

theorem DirichletTransform.TwoVariable.regRIntegral_smul_of_pos (t b₀ b₁ x y : ℂ) {a : ℝ} (ha : 0 < a) (hz : pair x y ∈ carlsonRVariableDomain) : regRIntegral t b₀ b₁ (↑a * x) (↑a * y) = ↑a ^ t * regRIntegral t b₀ b₁ x y

Positive-real homogeneity of the native regularized two-variable R-integral.

theorem DirichletTransform.TwoVariable.sub_mul_regRContinued_neg_one_one_one (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) : (y - x) * regCarlsonRContinued (-1) (pair x y) hz (pair 1 1) = Complex.log y - Complex.log x

The logarithmic base case in Carlson 8.5(2), without division by a node difference. Thus the identity also holds on the diagonal.

theorem DirichletTransform.TwoVariable.regRContinued_neg_one_one_one (x y : ℂ) (hz : pair x y ∈ carlsonRVariableDomain) (hxy : x ≠ y) : regCarlsonRContinued (-1) (pair x y) hz (pair 1 1) = (Complex.log y - Complex.log x) / (y - x)

Carlson's logarithmic elementary function, for distinct nodes.

theorem DirichletTransform.TwoVariable.regRContinued_neg_one_one_one_diag (x : ℂ) (hz : pair x x ∈ carlsonRVariableDomain) : regCarlsonRContinued (-1) (pair x x) hz (pair 1 1) = x⁻¹

The diagonal value completing the logarithmic base case.