Compactness of probability measures

Stream: maths

[Yaël Dillies]

Does anyone have work towards the compactness of the space of probability measures (under weak-* convergence) over a compact space? We have the finite space version in PFR but I think mathlib would enjoy getting the general version from the get go.

[Yaël Dillies]

cc @Kalle Kytölä, @Sébastien Gouëzel, @Rémy Degenne

[Sébastien Gouëzel]

For the general version, we need Riesz representation theorem, on which @Yoh Tanimoto is working if I understand correctly.

[Yoh Tanimoto]

yes, for that I will need #12266 or some variation of it

[Thomas Zhu]

I believe this is Lemma 2.8 of the central limit theorem blueprint, but it is not formalized at all

[Johan Commelin]

For my fellow readers: #12266 is help-wanted, and I think the request is explained here https://github.com/leanprover-community/mathlib4/pull/12266#discussion_r1807731828
If you have some experience with this area of mathlib, please see if you can help a bit.

[Yaël Dillies]

I will have a look on the 1st of november