instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace

English

Continuity of the inverse equivalence is established via a technical chain of lemmas about convergence of measures and thickening.

Русский

Доказано, что обратная эквивалентность непрерывна через цепочку лемм о сходимости мер и размытии.

LaTeX

$$$\\text{proof sketch: use lemmas on convergence in LP-space and measure-thickening bounds.}$$$

Lean4

/-- The topology of convergence in distribution on a separable space is pseudo-metrizable. -/
instance (X : Type*) [TopologicalSpace X] [PseudoMetrizableSpace X] [SeparableSpace X] [MeasurableSpace X]
    [OpensMeasurableSpace X] : PseudoMetrizableSpace (ProbabilityMeasure X) :=
  letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  (homeomorph_probabilityMeasure_levyProkhorov (Ω := X)).isInducing.pseudoMetrizableSpace

Похожие утверждения