Convergence of Carlson ray kernels

The products of powers in Carlson's single-integral representation (Section 6.8) have explicit power growth at infinity. These estimates also apply to the primitive used in the associated-function recurrence of Section 8.4.

noncomputable def DirichletTransform.carlsonRayProduct {ι : Type u_1} [Fintype ι] (c z : ι → ℂ) (x : ℝ) : ℂ

A product of principal powers of affine factors on a positive ray.

Equations

• DirichletTransform.carlsonRayProduct c z x = ∏ i : ι, (1 + ↑x * z i) ^ c i

theorem DirichletTransform.carlsonRayProduct_eq_scaled {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {x : ℝ} (hx : 0 < x) : carlsonRayProduct c z x = (↑x ^ ∑ i : ι, c i) * ∏ i : ι, ((↑x)⁻¹ + z i) ^ c i

Extracting the positive real scale from each affine factor is branch-safe.

theorem DirichletTransform.tendsto_carlsonRayProduct_scaled {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : Filter.Tendsto (fun (x : ℝ) => ∏ i : ι, ((↑x)⁻¹ + z i) ^ c i) Filter.atTop (nhds (∏ i : ι, z i ^ c i))

After removing its power growth, the ray product has a finite limit.

theorem DirichletTransform.isBigO_carlsonRayProduct_atTop {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : carlsonRayProduct c z =O[Filter.atTop] fun (x : ℝ) => x ^ (∑ i : ι, c i).re

A ray product has the growth predicted by the sum of the real parts of its exponents.

theorem DirichletTransform.continuousAt_carlsonRayProduct_zero {ι : Type u_1} [Fintype ι] (c z : ι → ℂ) : ContinuousAt (carlsonRayProduct c z) 0

At zero every affine factor tends to one.

theorem DirichletTransform.mellinConvergent_carlsonRayProduct {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℂ} (ha : 0 < a.re) (ha' : a.re + (∑ i : ι, c i).re < 0) : MellinConvergent (carlsonRayProduct c z) a

Absolute convergence of the Mellin integral of a ray product in its natural strip.

theorem DirichletTransform.tendsto_cpow_mul_carlsonRayProduct_atTop {ι : Type u_1} [Fintype ι] (a : ℂ) (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (ha : a.re + (∑ i : ι, c i).re < 0) : Filter.Tendsto (fun (x : ℝ) => ↑x ^ a * carlsonRayProduct c z x) Filter.atTop (nhds 0)

A power times a ray product tends to zero when its total growth exponent is negative.

noncomputable def DirichletTransform.carlsonRayDerivative {ι : Type u_1} [Fintype ι] (a : ℂ) (c z : ι → ℂ) (x : ℝ) : ℂ

The Leibniz derivative of a power times a ray product, with each differentiated factor represented by lowering just that factor's exponent.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.hasDerivAt_cpow_mul_carlsonRayProduct {ι : Type u_1} [Fintype ι] (a : ℂ) (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (x : ℝ) => ↑x ^ a * carlsonRayProduct c z x) (carlsonRayDerivative a c z x) x

Differentiation under the branch-safe positive-ray hypotheses.

theorem DirichletTransform.integrableOn_carlsonRayDerivative {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℂ} (ha : 0 < a.re) (ha' : a.re + (∑ i : ι, c i).re < 0) : MeasureTheory.IntegrableOn (carlsonRayDerivative a c z) (Set.Ioi 0) MeasureTheory.volume

The ray derivative is absolutely integrable in the boundary-vanishing strip.

theorem DirichletTransform.integral_carlsonRayDerivative_eq_zero {ι : Type u_1} [Fintype ι] (c : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {a : ℂ} (ha : 0 < a.re) (ha' : a.re + (∑ i : ι, c i).re < 0) : ∫ (x : ℝ) in Set.Ioi 0, carlsonRayDerivative a c z x = 0

Carlson's ray-kernel integration-by-parts identity. The hypotheses imply both endpoint values vanish and the derivative is absolutely integrable.

theorem DirichletTransform.mellin_carlsonRayProduct_eq_rIntegral {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (hsum : a + a' = ∑ i : ι, b i) (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : mellin (carlsonRayProduct (fun (i : ι) => -b i) z) a = a.betaIntegral a' * carlsonRIntegral (-a) b z

Carlson's Exercise 6.8-8: the ray representation with factors 1 + x zᵢ. This is the orientation needed in the proof of the associated-function recurrence.