Documentation

Mathlib.MeasureTheory.Measure.DiracProba

Dirac deltas as probability measures and embedding of a space into probability measures on it #

Main definitions #

Main results #

Tags #

probability measure, Dirac delta, embedding

theorem CompletelyRegularSpace.exists_BCNN {X : Type u_1} [TopologicalSpace X] [CompletelyRegularSpace X] {K : Set X} (K_closed : IsClosed K) {x : X} (x_notin_K : xK) :
∃ (f : BoundedContinuousFunction X NNReal), f x = 1 yK, f y = 0

The Dirac delta mass at a point x : X as a ProbabilityMeasure.

Equations
Instances For

    The assignment x ↦ diracProba x is injective if all singletons are measurable.

    @[simp]
    theorem MeasureTheory.diracProba_toMeasure_apply' {X : Type u_1} [MeasurableSpace X] (x : X) {A : Set X} (A_mble : MeasurableSet A) :
    (MeasureTheory.diracProba x) A = A.indicator 1 x
    @[simp]
    theorem MeasureTheory.diracProba_toMeasure_apply_of_mem {X : Type u_1} [MeasurableSpace X] {x : X} {A : Set X} (x_in_A : x A) :
    @[simp]
    theorem MeasureTheory.diracProba_toMeasure_apply {X : Type u_1} [MeasurableSpace X] [MeasurableSingletonClass X] (x : X) (A : Set X) :
    (MeasureTheory.diracProba x) A = A.indicator 1 x

    The assignment x ↦ diracProba x is continuous X → ProbabilityMeasure X.

    In a T0 topological space equipped with a sigma algebra which contains all open sets, the assignment x ↦ diracProba x is injective.

    noncomputable def MeasureTheory.diracProbaInverse {X : Type u_1} [MeasurableSpace X] :
    (Set.range MeasureTheory.diracProba)X

    An inverse function to diracProba (only really an inverse under hypotheses that guarantee injectivity of diracProba).

    Equations
    Instances For
      noncomputable def MeasureTheory.diracProbaEquiv {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] :
      X (Set.range MeasureTheory.diracProba)

      In a T0 topological space X, the assignment x ↦ diracProba x is a bijection to its range in ProbabilityMeasure X.

      Equations
      • MeasureTheory.diracProbaEquiv = { toFun := fun (x : X) => MeasureTheory.diracProba x, , invFun := MeasureTheory.diracProbaInverse, left_inv := , right_inv := }
      Instances For
        theorem MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_val {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] :
        MeasureTheory.diracProba MeasureTheory.diracProbaEquiv.symm = fun (μ : (Set.range MeasureTheory.diracProba)) => μ

        The composition of diracProbaEquiv.symm and diracProba is the subtype inclusion.

        theorem MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] [CompletelyRegularSpace X] {μ : (Set.range MeasureTheory.diracProba)} (F : Filter (Set.range MeasureTheory.diracProba)) :
        Filter.Tendsto (⇑MeasureTheory.diracProbaEquiv.symm) F (nhds (MeasureTheory.diracProbaEquiv.symm μ)) Filter.Tendsto id F (nhds μ)

        In a T0 topological space, diracProbaEquiv is continuous.

        In a completely regular T0 topological space, the inverse of diracProbaEquiv is continuous.

        noncomputable def MeasureTheory.diracProbaHomeomorph {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] [CompletelyRegularSpace X] :
        X ≃ₜ (Set.range MeasureTheory.diracProba)

        In a completely regular T0 topological space X, diracProbaEquiv is a homeomorphism to its image in ProbabilityMeasure X.

        Equations
        • MeasureTheory.diracProbaHomeomorph = { toEquiv := MeasureTheory.diracProbaEquiv, continuous_toFun := , continuous_invFun := }
        Instances For

          If X is a completely regular T0 space with its Borel sigma algebra, then the mapping that takes a point x : X to the delta-measure diracProba x is an embedding X → ProbabilityMeasure X.