The affine kernel for Carlson's Dirichlet averages

This file contains the common algebraic kernel used by both the real probability average and the complex regularized integral.

def DirichletTransform.carlsonAffineForm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) : ℂ

The affine form on the standard simplex associated with the complex parameters z.

Equations

• DirichletTransform.carlsonAffineForm z u = ∑ i : ι, ↑(u i) * z i

theorem DirichletTransform.continuous_carlsonAffineForm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : Continuous (carlsonAffineForm z)

The affine form associated with z is continuous in the simplex variable.

noncomputable def DirichletTransform.carlsonAffineFormCLM {ι : Type u_1} [Fintype ι] (u : ι → ℝ) : (ι → ℂ) →L[ℂ] ℂ

Carlson's affine form, regarded as a continuous complex-linear map in its node variables.

Equations

• DirichletTransform.carlsonAffineFormCLM u = ∑ i : ι, ↑(u i) • ContinuousLinearMap.proj i

theorem DirichletTransform.carlsonAffineFormCLM_apply {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (z : ι → ℂ) : (carlsonAffineFormCLM u) z = carlsonAffineForm z u

Evaluation of the continuous-linear version of Carlson's affine form.

theorem DirichletTransform.norm_carlsonAffineFormCLM_le_one {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : ‖carlsonAffineFormCLM u‖ ≤ 1

On the standard simplex, the operator norm of Carlson's affine form is at most one.

theorem DirichletTransform.dist_carlsonAffineForm_le_norm_sub {ι : Type u_1} [Fintype ι] (z w : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : dist (carlsonAffineForm w u) (carlsonAffineForm z u) ≤ ‖w - z‖

Moving the node vector moves every simplex affine combination by at most the supremum-norm distance between the node vectors.

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

A simplex affine combination is bounded by the supremum norm of its nodes.

noncomputable def DirichletTransform.carlsonSimplexCLM {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : (ι → ℝ) →L[ℝ] ℂ

Carlson's affine form as a real-linear map in its simplex coordinates.

Equations

• DirichletTransform.carlsonSimplexCLM z = ∑ k : ι, z k • Complex.ofRealCLM ∘SL ContinuousLinearMap.proj k

theorem DirichletTransform.carlsonSimplexCLM_apply {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) : (carlsonSimplexCLM z) u = carlsonAffineForm z u

Evaluation of the real-linear simplex-coordinate map.

theorem DirichletTransform.hasFDerivAt_carlsonSimplex {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) : HasFDerivAt (carlsonAffineForm z) (carlsonSimplexCLM z) u

The affine form has its defining real-linear map as its Fréchet derivative.

theorem DirichletTransform.carlsonSimplexCLM_tangent {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (i j : ι) : (carlsonSimplexCLM z) (Pi.single i 1 - Pi.single j 1) = z i - z j

A coordinate tangent vector is sent to the difference of the corresponding nodes.

theorem DirichletTransform.carlsonAffineForm_mem_convexHull {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : carlsonAffineForm z u ∈ (convexHull ℝ) (Set.range z)

Carlson's affine form lies in the real convex hull of its parameters.

theorem DirichletTransform.mem_convexHull_range_iff_carlsonAffineForm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (x : ℂ) : x ∈ (convexHull ℝ) (Set.range z) ↔ ∃ (u : Convexity.StdSimplex ℝ ι), carlsonAffineForm z u.coordinates = x

The convex hull of the nodes is exactly the image of the intrinsic simplex under Carlson's affine form, including for empty index types.

theorem DirichletTransform.zero_mem_convexHull_range_iff {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : 0 ∈ (convexHull ℝ) (Set.range z) ↔ ∃ (u : Convexity.StdSimplex ℝ ι), carlsonAffineForm z u.coordinates = 0

Zero lies in the convex hull precisely when the affine form vanishes at some simplex point.