Documentation

LeanPool.CarlsonFunctions.StdSimplexMeasure.IntrinsicMeasure

The coordinate-normalized measure on the intrinsic simplex #

The ambient MeasureTheory.Measure.stdSimplexMeasure is unchanged: it is a measure on the whole affine hyperplane, not merely on the simplex. This file pulls it back along the intrinsic coordinate embedding. Its pushforward is exactly the ambient measure restricted to the coordinate carrier.

No probability normalization is applied: for a nonempty index type the mass is 1 / (card ι - 1)!. Empty and singleton index types are included explicitly.

source
noncomputable def Convexity.StdSimplex.coordinateMeasure {ι : Type u_1} [Fintype ι] :
MeasureTheory.Measure (StdSimplex ℝ ι)

The intrinsic simplex measure, with the same free-coordinate normalization as the ambient hyperplane measure.

Equations
Instances For
    source
    theorem Convexity.StdSimplex.map_coordinates_coordinateMeasure {ι : Type u_1} [Fintype ι] :
    MeasureTheory.Measure.map coordinates coordinateMeasure = MeasureTheory.Measure.stdSimplexMeasure.restrict (coordinateSet ℝ ι)

    Embedding the intrinsic measure recovers the restricted ambient measure.

    source
    theorem Convexity.StdSimplex.measurePreserving_coordinates {ι : Type u_1} [Fintype ι] :
    MeasureTheory.MeasurePreserving coordinates coordinateMeasure (MeasureTheory.Measure.stdSimplexMeasure.restrict (coordinateSet ℝ ι))
    source
    theorem Convexity.StdSimplex.coordinateMeasure_apply {ι : Type u_1} [Fintype ι] (s : Set (StdSimplex ℝ ι)) :
    coordinateMeasure s = MeasureTheory.Measure.stdSimplexMeasure (coordinates '' s)
    source
    instance Convexity.StdSimplex.instIsFiniteMeasureRealCoordinateMeasure {ι : Type u_1} [Fintype ι] :
    MeasureTheory.IsFiniteMeasure coordinateMeasure
    source
    @[simp]
    theorem Convexity.StdSimplex.coordinateMeasure_univ {ι : Type u_1} [Fintype ι] [Nonempty ι] :
    coordinateMeasure Set.univ = 1 / ↑(Fintype.card ι - 1).factorial
    source
    @[simp]
    theorem Convexity.StdSimplex.coordinateMeasure_empty {ι : Type u_1} [Fintype ι] [IsEmpty ι] :
    coordinateMeasure = 0
    source
    theorem Convexity.StdSimplex.coordinateMeasure_univ_unique {ι : Type u_1} [Fintype ι] [Unique ι] :
    coordinateMeasure Set.univ = 1
    source
    theorem Convexity.StdSimplex.integral_coordinateMeasure {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) :
    ∫ (s : StdSimplex ℝ ι), f s.coordinates ∂coordinateMeasure = ∫ (u : ι → ℝ) in coordinateSet ℝ ι, f u ∂MeasureTheory.Measure.stdSimplexMeasure

    Integrating an ambient function over the intrinsic simplex is precisely the existing restricted hyperplane integral.