Commit 2024-05-20 22:00 abff007f

feat: Embed a space into probability measures on it. (#11815) Assuming a topological space X is completely regular and T0, it can be embedded into ProbabilityMeasure X. This shows in particular that for the Lévy-Prokhorov metrizability #11549 of ProbabilityMeasure X, certain assumptions cannot be relaxed. For example we have:

import Mathlib.MeasureTheory.Measure.DiracProba
variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [T0Space Ω] [CompletelyRegularSpace Ω]
open TopologicalSpace
example :
    ¬ MetrizableSpace Ω → ¬ MetrizableSpace (ProbabilityMeasure Ω) := by
  intro badSpace goodProba
  exact badSpace embedding_diracProba.metrizableSpace
example :
    ¬ PseudoMetrizableSpace Ω → ¬ PseudoMetrizableSpace (ProbabilityMeasure Ω) := by
  intro badSpace goodProba
  exact badSpace embedding_diracProba.pseudoMetrizableSpace
example :
    ¬ FirstCountableTopology Ω → ¬ FirstCountableTopology (ProbabilityMeasure Ω) := by
  intro badSpace goodProba
  exact badSpace embedding_diracProba.firstCountableTopology