Smooth functions and affine slices on the standard simplex

These geometric and calculus lemmas do not depend on Dirichlet densities or parameters. The historical DirichletTransform namespace is retained for compatibility.

def DirichletTransform.ContDiffNearStdSimplex {ι : Type u_1} [Fintype ι] (N : ℕ) (f : (ι → ℝ) → ℂ) : Prop

A function has N continuous derivatives near the closed standard simplex if it has that regularity on some open neighborhood of the simplex in the ambient coordinate space.

Equations

• DirichletTransform.ContDiffNearStdSimplex N f = ∃ (U : Set (ι → ℝ)), IsOpen U ∧ Convexity.StdSimplex.coordinateSet ℝ ι ⊆ U ∧ ContDiffOn ℝ (↑N) f U

theorem DirichletTransform.ContDiffNearStdSimplex.of_le {ι : Type u_1} [Fintype ι] {N M : ℕ} (hNM : N ≤ M) {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex M f) : ContDiffNearStdSimplex N f

Having more derivatives near the simplex implies having any smaller number of derivatives there.

theorem DirichletTransform.ContDiffNearStdSimplex.continuousOn {ι : Type u_1} [Fintype ι] {N : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex N f) : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)

Finite differentiability on a neighborhood implies continuity on the closed simplex.

Tangential derivatives

noncomputable def DirichletTransform.stdSimplexTangentVector {ι : Type u_1} (j k : ι) : ι → ℝ

The tangent vector to the simplex that increases coordinate j and decreases coordinate k at the same rate.

Equations

• DirichletTransform.stdSimplexTangentVector j k = Pi.single j 1 - Pi.single k 1

@[simp]

theorem DirichletTransform.sum_stdSimplexTangentVector {ι : Type u_1} [Fintype ι] (j k : ι) : ∑ i : ι, stdSimplexTangentVector j k i = 0

A simplex tangent vector has coordinate sum zero.

theorem DirichletTransform.stdSimplexTangentVector_comm {ι : Type u_1} (j k : ι) : stdSimplexTangentVector k j = -stdSimplexTangentVector j k

Reversing a simplex tangent direction negates it.

@[simp]

theorem DirichletTransform.stdSimplexTangentVector_self {ι : Type u_1} (j : ι) : stdSimplexTangentVector j j = 0

Transferring mass from a coordinate to itself gives the zero tangent vector.

noncomputable def DirichletTransform.stdSimplexTangentDeriv {ι : Type u_1} (j k : ι) (f : (ι → ℝ) → ℂ) (u : ι → ℝ) : ℂ

The ambient directional derivative in the tangent direction that transfers mass from coordinate k to coordinate j. Unlike a single coordinate derivative, this derivative is intrinsic to the affine hyperplane containing the simplex.

Equations

• DirichletTransform.stdSimplexTangentDeriv j k f u = (fderiv ℝ f u) (DirichletTransform.stdSimplexTangentVector j k)

theorem DirichletTransform.ContDiffNearStdSimplex.tangentDeriv {ι : Type u_1} [Fintype ι] {N : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex (N + 1) f) (j k : ι) : ContDiffNearStdSimplex N (stdSimplexTangentDeriv j k f)

Taking one tangential derivative consumes one order of differentiability near the simplex. This is the differential operator used in the boundary integration-by-parts recursion.

Boundary faces

noncomputable def DirichletTransform.stdSimplexFaceRestriction {ι : Type u_1} [Fintype ι] (i : ι) (f : (ι → ℝ) → ℂ) : ({ j : ι // j ≠ i } → ℝ) → ℂ

Restriction of a function to the face where coordinate i is zero. The remaining coordinates are indexed by {j // j ≠ i} and already sum to one on their standard simplex.

Equations

• DirichletTransform.stdSimplexFaceRestriction i f = f ∘ stdSimplexCoordMap i

theorem DirichletTransform.stdSimplexCoordMap_mem_face {ι : Type u_1} [Fintype ι] (i : ι) {v : { j : ι // j ≠ i } → ℝ} (hv : v ∈ Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }) : stdSimplexCoordMap i v ∈ Convexity.StdSimplex.coordinateSet ℝ ι

The coordinate map sends the smaller standard simplex onto the face where coordinate i is zero.

theorem DirichletTransform.stdSimplexCoordMap_face_apply_self {ι : Type u_1} [Fintype ι] (i : ι) {v : { j : ι // j ≠ i } → ℝ} (hv : v ∈ Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }) : stdSimplexCoordMap i v i = 0

On the smaller standard simplex, the inserted coordinate of the face map is zero.

theorem DirichletTransform.ContDiffNearStdSimplex.faceRestriction {ι : Type u_1} [Fintype ι] {N : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex N f) (i : ι) : ContDiffNearStdSimplex N (stdSimplexFaceRestriction i f)

Restricting to a boundary face preserves finite differentiability near the corresponding lower-dimensional standard simplex.

Slice parametrization

noncomputable def DirichletTransform.stdSimplexSlice {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) (f : (ι → ℝ) → ℂ) : ({ j : ι // j ≠ i } → ℝ) → ℂ

The affine line from the face u i = 0 to the vertex e i, parametrized so that the omitted coordinate equals t.

Equations

• DirichletTransform.stdSimplexSlice i t f v = f (stdSimplexCoordMap i fun (j : { j : ι // j ≠ i }) => (1 - t) * v j)

theorem DirichletTransform.stdSimplexSlice_zero {ι : Type u_1} [Fintype ι] (i : ι) (f : (ι → ℝ) → ℂ) : stdSimplexSlice i 0 f = stdSimplexFaceRestriction i f

theorem DirichletTransform.stdSimplexCoordMap_scale_eq_line {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) {v : { j : ι // j ≠ i } → ℝ} (hv : ∑ j : { j : ι // j ≠ i }, v j = 1) : (stdSimplexCoordMap i fun (j : { j : ι // j ≠ i }) => (1 - t) * v j) = t • Pi.single i 1 + (1 - t) • stdSimplexCoordMap i v

On the standard simplex of the complementary coordinates, the scaled chart is the line from the face point to the vertex Pi.single i 1.

theorem DirichletTransform.hasDerivAt_stdSimplexCoordMap_scale {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) {v : { j : ι // j ≠ i } → ℝ} (hv : ∑ j : { j : ι // j ≠ i }, v j = 1) : HasDerivAt (fun (s : ℝ) => stdSimplexCoordMap i fun (j : { j : ι // j ≠ i }) => (1 - s) * v j) (Pi.single i 1 - stdSimplexCoordMap i v) t

theorem DirichletTransform.ContDiffNearStdSimplex.slice {ι : Type u_1} [Fintype ι] {N : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex N f) (i : ι) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ContDiffNearStdSimplex N (stdSimplexSlice i t f)

Finite differentiability near the simplex is inherited by every slice.

theorem DirichletTransform.continuousOn_stdSimplexSlice {ι : Type u_1} [Fintype ι] (i : ι) {t : ℝ} (ht : t ∈ Set.Icc 0 1) {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : ContinuousOn (stdSimplexSlice i t f) (Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i })

Affine slices of a continuous simplex function remain continuous on the opposite face.

def DirichletTransform.powerPartitionDenom {ι : Type u_1} [Fintype ι] (M : ℕ) (u : ι → ℝ) : ℂ

The identity 1 = ∑ i, u i ^ M / powerPartitionDenom M u lets each term reserve enough powers of its omitted coordinate for all the subsequent parameter shifts.

Equations

• DirichletTransform.powerPartitionDenom M u = ∑ j : ι, ↑(u j) ^ M

theorem DirichletTransform.powerPartitionDenom_ne_zero {ι : Type u_1} [Fintype ι] (M : ℕ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : powerPartitionDenom M u ≠ 0

theorem DirichletTransform.contDiffNear_div_powerPartitionDenom {ι : Type u_1} [Fintype ι] {n : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex n f) (M : ℕ) : ContDiffNearStdSimplex n fun (u : ι → ℝ) => f u / powerPartitionDenom M u

theorem DirichletTransform.isClosed_stdSimplexFreeCoords {ι : Type u_1} [Fintype ι] (i : ι) : IsClosed (stdSimplexFreeCoords i)

theorem DirichletTransform.stdSimplexCoordMap_add_single {ι : Type u_1} [Fintype ι] (i : ι) (j : { j : ι // j ≠ i }) (x : { j : ι // j ≠ i } → ℝ) (t : ℝ) : stdSimplexCoordMap i (x + t • Pi.single j 1) = stdSimplexCoordMap i x + t • (Pi.single (↑j) 1 - Pi.single i 1)