The measurable structure of the standard simplex

A point of the standard simplex StdSimplex R ι is determined by its weight vector ι → R. This file gives the simplex the σ-algebra induced by that weight vector, for any coefficient type R carrying a measurable structure, so that a probability vector is a measurable parameter: the weight vector is measurable, and a map into the simplex is measurable exactly when its weight-vector map is.

The inverse weight map extends to all weight vectors by choosing a fallback simplex point. Its measurability under topological hypotheses is established in the Borel simplex file.

Mathlib's topology on the simplex is stated over a ring and does not reach coefficients such as ℝ≥0; the induced σ-algebra needs no topology.

Main declarations

• Convexity.StdSimplex.instMeasurableSpace — the σ-algebra induced by StdSimplex.weights;
• Convexity.StdSimplex.measurable_toFun_comp_weights — the weight vector is measurable;
• Convexity.StdSimplex.measurable_iff_toFun_comp_weights — measurability into the simplex is measurability of the weight vector;
• Convexity.StdSimplex.extendWeights — an inverse weight map with a chosen fallback.

@[instance_reducible]

instance Convexity.StdSimplex.instMeasurableSpace {R : Type u_1} {ι : Type u_2} [LE R] [AddCommMonoid R] [One R] [MeasurableSpace R] : MeasurableSpace (StdSimplex R ι)

The σ-algebra on the standard simplex induced by its weight vector.

theorem Convexity.StdSimplex.measurable_toFun_comp_weights {R : Type u_1} {ι : Type u_2} [LE R] [AddCommMonoid R] [One R] [MeasurableSpace R] : Measurable fun (p : StdSimplex R ι) => ⇑p.weights

The weight vector of a simplex point is measurable.

theorem Convexity.StdSimplex.measurable_iff_toFun_comp_weights {R : Type u_1} {ι : Type u_2} [LE R] [AddCommMonoid R] [One R] [MeasurableSpace R] {δ : Type u_3} [MeasurableSpace δ] {f : δ → StdSimplex R ι} : Measurable f ↔ Measurable fun (x : δ) => ⇑(f x).weights

A map into the simplex is measurable iff its weight-vector map is.

theorem Convexity.StdSimplex.injective_toFun_comp_weights {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] : Function.Injective fun (p : StdSimplex R ι) => ⇑p.weights

A simplex point is determined by its weight vector.

noncomputable def Convexity.StdSimplex.extendWeights {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] (p : StdSimplex R ι) (w : ι → R) : StdSimplex R ι

Read a weight vector as a simplex point when it lies in the simplex, using p elsewhere. This supplies probability parameters for mixtures supported on a simplex.

theorem Convexity.StdSimplex.extendWeights_def {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] (p : StdSimplex R ι) : p.extendWeights = Function.extend (fun (q : StdSimplex R ι) => ⇑q.weights) id fun (x : ι → R) => p

The inverse weight map is extended with constant fallback value p.

@[simp]

theorem Convexity.StdSimplex.extendWeights_weights {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] (p q : StdSimplex R ι) : p.extendWeights ⇑q.weights = q

Extending the inverse of the weight embedding recovers every simplex point.

@[simp]

theorem Convexity.StdSimplex.weights_extendWeights_of_mem_range {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] (p : StdSimplex R ι) {w : ι → R} (hw : w ∈ Set.range fun (q : StdSimplex R ι) => ⇑q.weights) : ⇑(p.extendWeights w).weights = w

Extending the inverse weight map preserves every vector in the simplex.

@[simp]

theorem Convexity.StdSimplex.extendWeights_of_notMem_range {R : Type u_1} {ι : Type u_2} [PartialOrder R] [Semiring R] (p : StdSimplex R ι) {w : ι → R} (hw : w ∉ Set.range fun (q : StdSimplex R ι) => ⇑q.weights) : p.extendWeights w = p

A vector outside the simplex is sent to the chosen fallback point.