Prokhorov theorem #32701

Stream: PR reviews

[Sébastien Gouëzel]

#32701 proves a version of Prokhorov theorem: given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set. We only assume that the space is T2 and normal (no metrizability, no second-countability). I know there is a version of this theorem in the central limit project, but with stronger assumptions, so instead I give a more conceptual proof using Riesz-Markov-Kakutani.

I have split a few preliminary PRs:

[Sébastien Gouëzel]

#32778 (+27/-4): show that Accumulate and partialSups coincide

[Sébastien Gouëzel]

#32779 (+62/-3): more consequences of Riesz-Markov-Kakutani

[Sébastien Gouëzel]

#32783 (+76/-26): for a regular measure, write the measure of an open set as a supremum of integrals of continuous functions

[Sébastien Gouëzel]

#32784 (+169/-3): more API for FiniteMeasure and ProbabilityMeasure

[Sébastien Gouëzel]

#32785 (+42/-0): a (finite or infinite) sum of inner regular measures is inner regular

[Sébastien Gouëzel]

#32786 (+11/-2): construct a bounded continuous map from a continuous compactly supported map

[Yaël Dillies]

How does this compare to @Arav Bhattacharyya's version, which is also based on RMK?

[Arav Bhattacharyya]

It’s more general I think - mine requires the second countable assumption as I was using a sequences proof

[Yaël Dillies]

Sébastien Gouëzel said:

#32786 (+11/-2): construct a bounded continuous map from a continuous compactly supported map

Why do you need this? I recently added a characterisation of weak convergence of measures on a compact space in terms of continuous functions

[Sébastien Gouëzel]

It's to apply RMK, which is phrased with compactly supported continuous functions. I need a uniform bound on the functions, so the simplest thing is to write ‖g.toBoundedContinuousFunction‖.