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

Main definitions

• diracProba: The Dirac delta mass at a point as a probability measure.

Main results

• isEmbedding_diracProba: 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.

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 : x ∉ K) : ∃ (f : BoundedContinuousFunction X NNReal), f x = 1 ∧ ∀ y ∈ K, f y = 0

noncomputable def MeasureTheory.diracProba {X : Type u_1} [MeasurableSpace X] (x : X) : ProbabilityMeasure X

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

Equations

• MeasureTheory.diracProba x = ⟨MeasureTheory.Measure.dirac x, ⋯⟩

theorem MeasureTheory.injective_diracProba {X : Type u_2} [MeasurableSpace X] [MeasurableSpace.SeparatesPoints X] : Function.Injective fun (x : X) => diracProba x

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) : ↑(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) : ↑(diracProba x) A = 1

@[simp]

theorem MeasureTheory.diracProba_toMeasure_apply {X : Type u_1} [MeasurableSpace X] [MeasurableSingletonClass X] (x : X) (A : Set X) : ↑(diracProba x) A = A.indicator 1 x

theorem MeasureTheory.continuous_diracProba {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] : Continuous fun (x : X) => diracProba x

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

theorem MeasureTheory.injective_diracProba_of_T0 {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] : Function.Injective fun (x : X) => diracProba x

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

theorem MeasureTheory.not_tendsto_diracProba_of_not_tendsto {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompletelyRegularSpace X] {x : X} (L : Filter X) (h : ¬Filter.Tendsto id L (nhds x)) : ¬Filter.Tendsto diracProba L (nhds (diracProba x))

theorem MeasureTheory.tendsto_diracProba_iff_tendsto {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompletelyRegularSpace X] {x : X} (L : Filter X) : Filter.Tendsto diracProba L (nhds (diracProba x)) ↔ Filter.Tendsto id L (nhds x)

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

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

Equations

• MeasureTheory.diracProbaInverse μ' = ⋯.choose

@[simp]

theorem MeasureTheory.diracProba_diracProbaInverse {X : Type u_2} [MeasurableSpace X] (μ : ↑(Set.range diracProba)) : diracProba (diracProbaInverse μ) = ↑μ

theorem MeasureTheory.diracProbaInverse_eq {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] {x : X} {μ : ↑(Set.range diracProba)} (h : ↑μ = diracProba x) : diracProbaInverse μ = x

noncomputable def MeasureTheory.diracProbaEquiv {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] : X ≃ ↑(Set.range 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 := ⋯ }

theorem MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_val {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] : diracProba ∘ ⇑diracProbaEquiv.symm = fun (μ : ↑(Set.range 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 diracProba)} (F : Filter ↑(Set.range diracProba)) : Filter.Tendsto (⇑diracProbaEquiv.symm) F (nhds (diracProbaEquiv.symm μ)) ↔ Filter.Tendsto id F (nhds μ)

theorem MeasureTheory.continuous_diracProbaEquiv {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] : Continuous ⇑diracProbaEquiv

In a T0 topological space, diracProbaEquiv is continuous.

theorem MeasureTheory.continuous_diracProbaEquivSymm {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] [CompletelyRegularSpace X] : Continuous ⇑diracProbaEquiv.symm

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 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 := ⋯ }

theorem MeasureTheory.isEmbedding_diracProba {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] [CompletelyRegularSpace X] : Topology.IsEmbedding fun (x : X) => diracProba x

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.