Carlson's R-function: homogeneity and associated-function relations

This file proves the regularized forms of Carlson's formulas 5.9-3, 5.9-5, and 5.9-6 on the native convergence region and right-half-plane node domain. The third associated relation follows by summing the tangential integration-by-parts relation. All three algebraic associated relations are also extended to arbitrary complex Dirichlet parameters for regCarlsonRContinued. Node derivatives are still stated for the native integral.

theorem DirichletTransform.regCarlsonRIntegral_eq_sum_update_add_one {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonRIntegral t b z = ∑ i : ι, b i * regCarlsonRIntegral t (Function.update b i (b i + 1)) z

Carlson's first associated-function relation 5.9-5, in regularized form. Gamma regularization absorbs Carlson's weights and leaves the coefficients b i.

theorem DirichletTransform.regCarlsonRIntegral_add_one_eq_sum_mul_update {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonRIntegral (t + 1) b z = ∑ i : ι, b i * z i * regCarlsonRIntegral t (Function.update b i (b i + 1)) z

Carlson's second associated-function relation 5.9-5, in regularized form.

theorem DirichletTransform.regCarlsonRIntegral_tangent {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i j : ι) : (z i - z j) * (t * regCarlsonRIntegral (t - 1) (addDirichletUnit (addDirichletUnit b i) j) z) = regCarlsonRIntegral t (addDirichletUnit b i) z - regCarlsonRIntegral t (addDirichletUnit b j) z

The tangential contiguous relation for the power kernel, including equal indices.

theorem DirichletTransform.regCarlsonRIntegral_eq_update_add_one {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i : ι) : regCarlsonRIntegral t b z = (∑ j : ι, b j + t) * regCarlsonRIntegral t (addDirichletUnit b i) z - t * z i * regCarlsonRIntegral (t - 1) (addDirichletUnit b i) z

Carlson's third associated-function relation 5.9-5, equation (7), in regularized form. No parameter is lowered, so the ordinary convergence hypothesis suffices.

theorem DirichletTransform.mul_carlsonPartialDeriv_add_mul_regCarlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (i : ι) : z i * carlsonPartialDeriv i (regCarlsonRIntegral t b) z + b i * regCarlsonRIntegral t b z = b i * (∑ j : ι, b j + t) * regCarlsonRIntegral t (addDirichletUnit b i) z

Carlson's second differential relation 5.9-6, equation (10), in regularized form. The first relation, equation (9), is carlsonPartialDeriv_regCarlsonRIntegral.

theorem DirichletTransform.sum_carlsonPartialDeriv_regCarlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ i : ι, carlsonPartialDeriv i (regCarlsonRIntegral t b) z = t * regCarlsonRIntegral (t - 1) b z

Carlson's translation differential identity, the first equation of Theorem 5.9-2.

theorem DirichletTransform.sum_mul_carlsonPartialDeriv_regCarlsonRIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ i : ι, z i * carlsonPartialDeriv i (regCarlsonRIntegral t b) z = t * regCarlsonRIntegral t b z

Carlson's Euler differential identity, the second equation of Theorem 5.9-2, for the native regularized R integral.

theorem DirichletTransform.regCarlsonRContinued_eq_sum_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued t z hz b = ∑ i : ι, b i * regCarlsonRContinued t z hz (addDirichletUnit b i)

The first associated relation holds for the continued function at every complex Dirichlet parameter, including points outside the native convergence region.

theorem DirichletTransform.regCarlsonRContinued_add_one_eq_sum_mul_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued (t + 1) z hz b = ∑ i : ι, b i * z i * regCarlsonRContinued t z hz (addDirichletUnit b i)

The second associated relation extends to all complex Dirichlet parameters.

theorem DirichletTransform.regCarlsonRContinued_eq_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i : ι) : regCarlsonRContinued t z hz b = (∑ j : ι, b j + t) * regCarlsonRContinued t z hz (addDirichletUnit b i) - t * z i * regCarlsonRContinued (t - 1) z hz (addDirichletUnit b i)

Carlson's third associated relation holds everywhere in the Dirichlet parameters after regularization; no division by the total parameter or by the exponent is needed.

theorem DirichletTransform.ofReal_pos_mul_cpow (t w : ℂ) {a : ℝ} (ha : 0 < a) (hw : w ≠ 0) : (↑a * w) ^ t = ↑a ^ t * w ^ t

Positive-real scaling commutes with the principal complex power.

theorem DirichletTransform.cpow_carlsonAffineForm_smul {ι : Type u_1} [Fintype ι] (t : ℂ) {a : ℝ} (ha : 0 < a) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : carlsonAffineForm (fun (i : ι) => ↑a * z i) u ^ t = ↑a ^ t * carlsonAffineForm z u ^ t

Pointwise homogeneity of Carlson's power kernel for positive real scaling.

theorem DirichletTransform.regCarlsonRIntegral_smul_of_pos {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℝ} (ha : 0 < a) : (regCarlsonRIntegral t b fun (i : ι) => ↑a * z i) = ↑a ^ t * regCarlsonRIntegral t b z

Carlson's homogeneity formula 5.9-3 for the native regularized integral, stated with positive real scaling so that Mathlib's principal branch is preserved.

theorem DirichletTransform.carlsonRIntegral_smul_of_pos {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℝ} (ha : 0 < a) : (carlsonRIntegral t b fun (i : ι) => ↑a * z i) = ↑a ^ t * carlsonRIntegral t b z

The corresponding unregularized homogeneity formula.

theorem DirichletTransform.mul_cpow_of_re_pos {a w : ℂ} (ha : 0 < a.re) (hw : 0 < w.re) (t : ℂ) : (a * w) ^ t = a ^ t * w ^ t

Two factors in the right half-plane have compatible principal logarithms.

theorem DirichletTransform.regCarlsonRIntegral_smul_of_re_pos {ι : Type u_1} [Fintype ι] (t : ℂ) {a : ℂ} (ha : 0 < a.re) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : (regCarlsonRIntegral t b fun (i : ι) => a * z i) = a ^ t * regCarlsonRIntegral t b z

Complex homogeneity on the right half-plane, with explicit principal-branch control. The scaled variables need not themselves be in the right half-plane.

theorem DirichletTransform.carlsonRIntegral_smul_of_re_pos {ι : Type u_1} [Fintype ι] (t : ℂ) {a : ℂ} (ha : 0 < a.re) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : (carlsonRIntegral t b fun (i : ι) => a * z i) = a ^ t * carlsonRIntegral t b z

Unregularized complex homogeneity with the same principal-branch hypotheses.