Documentation

PFR.ForMathlib.CompactProb

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 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) μ))

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.
Instances For

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

    Equations
    Instances For

      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.