Carlson's Dirichlet averages: basic definitions

This file specializes the regularized Dirichlet integral to a univariate function evaluated at the affine form ∑ i, u i * z i. It contains the algebraic and convex-geometric material used by both the native integral theory of Carlson's Chapter 5 and its analytic continuation in Chapter 6.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Chapters 5 and 6, Academic Press, 1977.

noncomputable def DirichletTransform.carlsonAffinePolynomial {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : MvPolynomial ι ℂ

The multivariate polynomial whose value is Carlson's affine form.

Equations

• DirichletTransform.carlsonAffinePolynomial z = ∑ i : ι, MvPolynomial.C (z i) * MvPolynomial.X i

@[simp]

theorem DirichletTransform.eval_carlsonAffinePolynomial {ι : Type u_1} [Fintype ι] (z x : ι → ℂ) : (MvPolynomial.eval x) (carlsonAffinePolynomial z) = ∑ i : ι, x i * z i

Evaluation of carlsonAffinePolynomial gives the corresponding affine form.

noncomputable def DirichletTransform.carlsonPowerPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) : MvPolynomial ι ℂ

The polynomial representing the nth power of Carlson's affine form.

Equations

• DirichletTransform.carlsonPowerPolynomial n z = DirichletTransform.carlsonAffinePolynomial z ^ n

@[simp]

theorem DirichletTransform.eval_carlsonPowerPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) (u : ι → ℝ) : (MvPolynomial.eval fun (i : ι) => ↑(u i)) (carlsonPowerPolynomial n z) = carlsonAffineForm z u ^ n

Evaluation of carlsonPowerPolynomial gives the corresponding power of the affine form.

noncomputable def DirichletTransform.regCarlsonDirichletAverage {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (f : ℂ → ℂ) : ℂ

Carlson's Dirichlet average divided by Γ(∑ i, b i), on the native integral domain.

The function supplied to the simplex integral is u ↦ f (∑ i, u i * z i).

Equations

• DirichletTransform.regCarlsonDirichletAverage b z f = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => f (DirichletTransform.carlsonAffineForm z u)

noncomputable def DirichletTransform.carlsonDirichletAverage {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (f : ℂ → ℂ) : ℂ

Carlson's native (unregularized) Dirichlet average on the convergence region.

Equations

• DirichletTransform.carlsonDirichletAverage b z f = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonDirichletAverage b z f

The native averaging process

@[simp]

theorem DirichletTransform.carlsonAffineForm_perm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (σ : Equiv.Perm ι) (u : ι → ℝ) : carlsonAffineForm (z ∘ ⇑σ) (u ∘ ⇑σ) = carlsonAffineForm z u

Simultaneously permuting the simplex coordinates and the parameters of the affine form does not change that affine form.

theorem DirichletTransform.carlsonAffineForm_const {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) (w : ℂ) : carlsonAffineForm (fun (x : ι) => w) u = w

The affine form of a constant parameter vector is constant on the standard simplex.

theorem DirichletTransform.regCarlsonDirichletAverage_perm {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (f : ℂ → ℂ) (σ : Equiv.Perm ι) : regCarlsonDirichletAverage (b ∘ ⇑σ) (z ∘ ⇑σ) f = regCarlsonDirichletAverage b z f

Simultaneous permutation of the Dirichlet parameters and the variables leaves the native regularized Carlson average unchanged. This is the regularized form of Carlson's Theorem 5.2-3.

theorem DirichletTransform.regCarlsonDirichletAverage_const {ι : Type u_1} [Fintype ι] (f : ℂ → ℂ) (w : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonDirichletAverage b (fun (x : ι) => w) f = f w / Complex.Gamma (∑ i : ι, b i)

On the diagonal, the native regularized Carlson average is f(w) / Γ(∑ i, b i). This is the regularized form of Carlson's equation (5.2-2).

theorem DirichletTransform.carlsonAffineForm_affine {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) (a t : ℂ) (z : ι → ℂ) : carlsonAffineForm (fun (i : ι) => a * z i + t) u = a * carlsonAffineForm z u + t

Affine changes in the variables commute with Carlson's affine form on the standard simplex.

theorem DirichletTransform.regCarlsonDirichletAverage_comp_affine {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (f : ℂ → ℂ) (a t : ℂ) : (regCarlsonDirichletAverage b z fun (w : ℂ) => f (a * w + t)) = regCarlsonDirichletAverage b (fun (i : ι) => a * z i + t) f

Precomposing the averaged function by an affine map is equivalent to applying the same affine map to every variable. This is Carlson's Theorem 5.2-6.

theorem DirichletTransform.norm_carlsonAffineForm_le_sum_norm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : ‖carlsonAffineForm z u‖ ≤ ∑ i : ι, ‖z i‖

On the standard simplex, Carlson's affine form is bounded by the sum of the norms of its variables.

theorem DirichletTransform.sub_carlsonAffineForm_ne_zero {ι : Type u_1} [Fintype ι] {s : ℂ} {z : ι → ℂ} {u : ι → ℝ} (hs : s ∉ (convexHull ℝ) (Set.range z)) (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : s - carlsonAffineForm z u ≠ 0

The denominator in Carlson's resolvent is nonzero off the convex hull of z.

def DirichletTransform.carlsonRightHalfPlane : Set ℂ

The open right half-plane, an important domain for Carlson's power and resolvent constructions.

Equations

• DirichletTransform.carlsonRightHalfPlane = {w : ℂ | 0 < w.re}

theorem DirichletTransform.isOpen_carlsonRightHalfPlane : IsOpen carlsonRightHalfPlane

The right half-plane is open.

theorem DirichletTransform.convex_carlsonRightHalfPlane : Convex ℝ carlsonRightHalfPlane

The right half-plane is convex over the real scalars.

def DirichletTransform.HolomorphicOnCarlsonRightHalfPlane (f : ℂ → ℂ) : Prop

A convenient name for the hypothesis that a univariate function is holomorphic on the right half-plane.

Equations

• DirichletTransform.HolomorphicOnCarlsonRightHalfPlane f = AnalyticOnNhd ℂ f DirichletTransform.carlsonRightHalfPlane

theorem DirichletTransform.regCarlsonDirichletAverage_const_mul {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (c : ℂ) (f : ℂ → ℂ) : (regCarlsonDirichletAverage b z fun (w : ℂ) => c * f w) = c * regCarlsonDirichletAverage b z f

A complex scalar can be pulled through a regularized Carlson average.

theorem DirichletTransform.regCarlsonDirichletAverage_finsetSum {ι : Type u_1} [Fintype ι] {κ : Type u_2} {s : Finset κ} {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (f : κ → ℂ → ℂ) (hf : ∀ k ∈ s, ContinuousOn (fun (u : ι → ℝ) => f k (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)) : (regCarlsonDirichletAverage b z fun (w : ℂ) => ∑ k ∈ s, f k w) = ∑ k ∈ s, regCarlsonDirichletAverage b z (f k)

A finite sum can be passed through a regularized Carlson average on the native convergence domain.