Measurable simplex embeddings and the nonnegative-real Borel structure

For finite coordinate types with topologically measurable coefficients, the weight map is a measurable embedding. Its inverse extends measurably to all weight vectors by choosing a fallback simplex point; this permits mixing distributions against simplex-supported laws.

The weight-coordinate measurable structure on Convexity.StdSimplex ℝ≥0 ι agrees with the Borel structure of its coordinate topology when ι is finite. Thus continuous families of probability vectors also give measurable parameters for finite laws.

theorem Convexity.StdSimplex.measurableEmbedding_toFun_comp_weights {ι : Type u_1} [Finite ι] {R : Type u_2} [PartialOrder R] [Semiring R] [MeasurableSpace R] [TopologicalSpace R] [OpensMeasurableSpace R] [OrderClosedTopology R] [ContinuousAdd R] [SecondCountableTopology R] : MeasurableEmbedding fun (p : StdSimplex R ι) => ⇑p.weights

The weight vector embeds a finite standard simplex as a measurable subset of the coordinate space.

theorem Convexity.StdSimplex.measurable_extendWeights {ι : Type u_1} [Finite ι] {R : Type u_2} [PartialOrder R] [Semiring R] [MeasurableSpace R] [TopologicalSpace R] [OpensMeasurableSpace R] [OrderClosedTopology R] [ContinuousAdd R] [SecondCountableTopology R] (p : StdSimplex R ι) : Measurable p.extendWeights

The extension of the inverse weight map is measurable, including outside the simplex.

instance Convexity.StdSimplex.instBorelSpaceNNReal {ι : Type u_1} [Finite ι] : BorelSpace (StdSimplex NNReal ι)

The coordinate measurable structure of the finite nonnegative-real simplex is Borel.