Weak limits carried by Hausdorff limits of compact sets #
The full compact carrier is retained, even when the limiting measure has smaller support. Restriction to the carrier is an actual comap probability measure whose inclusion pushforward recovers the ambient probability.
Adapted from Freezing2/Probability/CompactSupportLimit.lean in
igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit
8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).
theorem
BGW.MetricMeasure.probabilityMeasure_compact_limit_eq_one
{X : Type u_1}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
{μ : ℕ → MeasureTheory.ProbabilityMeasure X}
{ν : MeasureTheory.ProbabilityMeasure X}
{S : ℕ → TopologicalSpace.NonemptyCompacts X}
{L : TopologicalSpace.NonemptyCompacts X}
(hμ : Filter.Tendsto μ Filter.atTop (nhds ν))
(hS : Filter.Tendsto S Filter.atTop (nhds L))
(hs : ∀ (n : ℕ), ↑(μ n) ↑(S n) = 1)
:
Simultaneous weak and Hausdorff convergence preserves concentration on the limiting compact carrier; no full-support hypothesis is needed.
theorem
BGW.MetricMeasure.exists_probabilityMeasure_on_compact
{X : Type u_1}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
(ν : MeasureTheory.ProbabilityMeasure X)
(L : TopologicalSpace.NonemptyCompacts X)
(hν : ↑ν ↑L = 1)
:
∃ (η : MeasureTheory.ProbabilityMeasure ↥L), MeasureTheory.Measure.map (fun (x : ↥L) => ↑x) ↑η = ↑ν
Restrict a probability carried by a compact set to that entire set. Points of mass zero are retained in the subtype.