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.

theorem continuous_pmf_apply' {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] (i : X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => (↑μ).real {i}

theorem continuous_pmf_apply {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] (i : X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => μ {i}

theorem tendsto_lintegral_of_forall_of_finite {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] [Finite X] {ι : Type u_2} {L : Filter ι} (μs : ι → MeasureTheory.Measure X) (μ : MeasureTheory.Measure X) (f : BoundedContinuousFunction X NNReal) (h : ∀ (x : X), Filter.Tendsto (fun (i : ι) => (μs i) {x}) L (nhds (μ {x}))) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : X), ↑(f x) ∂μs i) L (nhds (∫⁻ (x : X), ↑(f x) ∂μ))

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.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯