Compactness of the space of probability measures

We define the canonical bijection between the space of probability measures on a finite space X and the standard simplex, and show that it is a homeomorphism.

We deduce that the space of probability measures is compact in this situation. This is an easy case of a result that holds in a general compact metrizable space, but requires Riesz representation theorem which we don't have currently in mathlib.

noncomputable def probabilityMeasureEquivStdSimplex {X : Type u_1} [MeasurableSpace X] [Fintype X] [MeasurableSingletonClass X] : MeasureTheory.ProbabilityMeasure X ≃ ↑(stdSimplex ℝ X)

The canonical bijection between the set of probability measures on a fintype and the set of nonnegative functions on the points adding up to one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem probabilityMeasureEquivStdSimplex_symm_coe_apply {X : Type u_1} [MeasurableSpace X] [Fintype X] [MeasurableSingletonClass X] (p : ↑(stdSimplex ℝ X)) : ↑(probabilityMeasureEquivStdSimplex.symm p) = ∑ i : X, ENNReal.ofReal (p i) • MeasureTheory.Measure.dirac i

@[simp]

theorem probabilityMeasureEquivStdSimplex_coe_apply {X : Type u_1} [MeasurableSpace X] [Fintype X] [MeasurableSingletonClass X] (μ : MeasureTheory.ProbabilityMeasure X) (i : X) : (probabilityMeasureEquivStdSimplex μ) i = ↑(μ {i})

noncomputable def probabilityMeasureHomeoStdSimplex {X : Type u_1} [MeasurableSpace X] [Fintype X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] : MeasureTheory.ProbabilityMeasure X ≃ₜ ↑(stdSimplex ℝ X)

The canonical homeomorphism between the space of probability measures on a finite space and the standard simplex.

Equations

• probabilityMeasureHomeoStdSimplex = { toEquiv := probabilityMeasureEquivStdSimplex, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance instCompactSpaceProbabilityMeasure_pFR {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [Finite X] [DiscreteTopology X] [BorelSpace X] : CompactSpace (MeasureTheory.ProbabilityMeasure X)

This is still true when X is a metrizable compact space, but the proof requires Riesz representation theorem. TODO: remove once the general version is proved.

instance instSecondCountableTopologyProbabilityMeasure_pFR {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [Finite X] [DiscreteTopology X] [BorelSpace X] : SecondCountableTopology (MeasureTheory.ProbabilityMeasure X)