|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Kalle Kytölä. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kalle Kytölä |
| 5 | +-/ |
| 6 | +import Mathlib.Topology.CompletelyRegular |
| 7 | +import Mathlib.MeasureTheory.Measure.ProbabilityMeasure |
| 8 | + |
| 9 | +/-! |
| 10 | +# Dirac deltas as probability measures and embedding of a space into probability measures on it |
| 11 | +
|
| 12 | +## Main definitions |
| 13 | +* `diracProba`: The Dirac delta mass at a point as a probability measure. |
| 14 | +
|
| 15 | +## Main results |
| 16 | +* `embedding_diracProba`: If `X` is a completely regular T0 space with its Borel sigma algebra, |
| 17 | + then the mapping that takes a point `x : X` to the delta-measure `diracProba x` is an embedding |
| 18 | + `X ↪ ProbabilityMeasure X`. |
| 19 | +
|
| 20 | +## Tags |
| 21 | +probability measure, Dirac delta, embedding |
| 22 | +-/ |
| 23 | + |
| 24 | +open Topology Metric Filter Set ENNReal NNReal BoundedContinuousFunction |
| 25 | + |
| 26 | +open scoped Topology ENNReal NNReal BoundedContinuousFunction |
| 27 | + |
| 28 | +lemma CompletelyRegularSpace.exists_BCNN {X : Type*} [TopologicalSpace X] [CompletelyRegularSpace X] |
| 29 | + {K : Set X} (K_closed : IsClosed K) {x : X} (x_notin_K : x ∉ K) : |
| 30 | + ∃ (f : X →ᵇ ℝ≥0), f x = 1 ∧ (∀ y ∈ K, f y = 0) := by |
| 31 | + obtain ⟨g, g_cont, gx_zero, g_one_on_K⟩ := |
| 32 | + CompletelyRegularSpace.completely_regular x K K_closed x_notin_K |
| 33 | + have g_bdd : ∀ x y, dist (Real.toNNReal (g x)) (Real.toNNReal (g y)) ≤ 1 := by |
| 34 | + refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_ |
| 35 | + simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop |
| 36 | + set g' := BoundedContinuousFunction.mkOfBound |
| 37 | + ⟨fun x ↦ Real.toNNReal (g x), continuous_real_toNNReal.comp g_cont.subtype_val⟩ 1 g_bdd |
| 38 | + set f := 1 - g' |
| 39 | + refine ⟨f, by simp [f, g', gx_zero], fun y y_in_K ↦ by simp [f, g', g_one_on_K y_in_K]⟩ |
| 40 | + |
| 41 | +namespace MeasureTheory |
| 42 | + |
| 43 | +section embed_to_probabilityMeasure |
| 44 | + |
| 45 | +variable {X : Type*} [MeasurableSpace X] |
| 46 | + |
| 47 | +/-- The Dirac delta mass at a point `x : X` as a `ProbabilityMeasure`. -/ |
| 48 | +noncomputable def diracProba (x : X) : ProbabilityMeasure X := |
| 49 | + ⟨Measure.dirac x, Measure.dirac.isProbabilityMeasure⟩ |
| 50 | + |
| 51 | +/-- The assignment `x ↦ diracProba x` is injective if all singletons are measurable. -/ |
| 52 | +lemma injective_diracProba {X : Type*} [MeasurableSpace X] [MeasurableSpace.SeparatesPoints X] : |
| 53 | + Function.Injective (fun (x : X) ↦ diracProba x) := by |
| 54 | + intro x y x_eq_y |
| 55 | + rw [← dirac_eq_dirac_iff] |
| 56 | + rwa [Subtype.ext_iff] at x_eq_y |
| 57 | + |
| 58 | +@[simp] lemma diracProba_toMeasure_apply' (x : X) {A : Set X} (A_mble : MeasurableSet A) : |
| 59 | + (diracProba x).toMeasure A = A.indicator 1 x := Measure.dirac_apply' x A_mble |
| 60 | + |
| 61 | +@[simp] lemma diracProba_toMeasure_apply_of_mem {x : X} {A : Set X} (x_in_A : x ∈ A) : |
| 62 | + (diracProba x).toMeasure A = 1 := Measure.dirac_apply_of_mem x_in_A |
| 63 | + |
| 64 | +@[simp] lemma diracProba_toMeasure_apply [MeasurableSingletonClass X] (x : X) (A : Set X) : |
| 65 | + (diracProba x).toMeasure A = A.indicator 1 x := Measure.dirac_apply _ _ |
| 66 | + |
| 67 | +variable [TopologicalSpace X] [OpensMeasurableSpace X] |
| 68 | + |
| 69 | +/-- The assignment `x ↦ diracProba x` is continuous `X → ProbabilityMeasure X`. -/ |
| 70 | +lemma continuous_diracProba : Continuous (fun (x : X) ↦ diracProba x) := by |
| 71 | + rw [continuous_iff_continuousAt] |
| 72 | + apply fun x ↦ ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr fun f ↦ ?_ |
| 73 | + have f_mble : Measurable (fun X ↦ (f X : ℝ≥0∞)) := |
| 74 | + measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable |
| 75 | + simp only [diracProba, ProbabilityMeasure.coe_mk, lintegral_dirac' _ f_mble] |
| 76 | + exact (ENNReal.continuous_coe.comp f.continuous).continuousAt |
| 77 | + |
| 78 | +/-- In a T0 topological space equipped with a sigma algebra which contains all open sets, |
| 79 | +the assignment `x ↦ diracProba x` is injective. -/ |
| 80 | +lemma injective_diracProba_of_T0 [T0Space X] : |
| 81 | + Function.Injective (fun (x : X) ↦ diracProba x) := by |
| 82 | + intro x y δx_eq_δy |
| 83 | + by_contra x_ne_y |
| 84 | + exact dirac_ne_dirac x_ne_y <| congr_arg Subtype.val δx_eq_δy |
| 85 | + |
| 86 | +lemma not_tendsto_diracProba_of_not_tendsto [CompletelyRegularSpace X] {x : X} (L : Filter X) |
| 87 | + (h : ¬ Tendsto id L (𝓝 x)) : |
| 88 | + ¬ Tendsto diracProba L (𝓝 (diracProba x)) := by |
| 89 | + obtain ⟨U, U_nhd, hU⟩ : ∃ U, U ∈ 𝓝 x ∧ ∃ᶠ x in L, x ∉ U := by |
| 90 | + by_contra! con |
| 91 | + apply h |
| 92 | + intro U U_nhd |
| 93 | + simpa only [not_frequently, not_not] using con U U_nhd |
| 94 | + have Uint_nhd : interior U ∈ 𝓝 x := by simpa only [interior_mem_nhds] using U_nhd |
| 95 | + obtain ⟨f, fx_eq_one, f_vanishes_outside⟩ := |
| 96 | + CompletelyRegularSpace.exists_BCNN isOpen_interior.isClosed_compl |
| 97 | + (by simpa only [mem_compl_iff, not_not] using mem_of_mem_nhds Uint_nhd) |
| 98 | + rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, not_forall] |
| 99 | + use f |
| 100 | + simp only [diracProba, ProbabilityMeasure.coe_mk, fx_eq_one, |
| 101 | + lintegral_dirac' _ (measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable)] |
| 102 | + apply not_tendsto_iff_exists_frequently_nmem.mpr |
| 103 | + refine ⟨Ioi 0, Ioi_mem_nhds (by simp only [ENNReal.coe_one, zero_lt_one]), |
| 104 | + hU.mp (eventually_of_forall ?_)⟩ |
| 105 | + intro x x_notin_U |
| 106 | + rw [f_vanishes_outside x |
| 107 | + (compl_subset_compl.mpr (show interior U ⊆ U from interior_subset) x_notin_U)] |
| 108 | + simp only [ENNReal.coe_zero, mem_Ioi, lt_self_iff_false, not_false_eq_true] |
| 109 | + |
| 110 | +lemma tendsto_diracProba_iff_tendsto [CompletelyRegularSpace X] {x : X} (L : Filter X) : |
| 111 | + Tendsto diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x) := by |
| 112 | + constructor |
| 113 | + · contrapose |
| 114 | + exact not_tendsto_diracProba_of_not_tendsto L |
| 115 | + · intro h |
| 116 | + have aux := (@continuous_diracProba X _ _ _).continuousAt (x := x) |
| 117 | + simp only [ContinuousAt] at aux |
| 118 | + exact aux.comp h |
| 119 | + |
| 120 | +/-- An inverse function to `diracProba` (only really an inverse under hypotheses that |
| 121 | +guarantee injectivity of `diracProba`). -/ |
| 122 | +noncomputable def diracProbaInverse : range (diracProba (X := X)) → X := |
| 123 | + fun μ' ↦ (mem_range.mp μ'.prop).choose |
| 124 | + |
| 125 | +@[simp] lemma diracProba_diracProbaInverse (μ : range (diracProba (X := X))) : |
| 126 | + diracProba (diracProbaInverse μ) = μ := (mem_range.mp μ.prop).choose_spec |
| 127 | + |
| 128 | +lemma diracProbaInverse_eq [T0Space X] {x : X} {μ : range (diracProba (X := X))} |
| 129 | + (h : μ = diracProba x) : |
| 130 | + diracProbaInverse μ = x := by |
| 131 | + apply injective_diracProba_of_T0 (X := X) |
| 132 | + simp only [← h] |
| 133 | + exact (mem_range.mp μ.prop).choose_spec |
| 134 | + |
| 135 | +/-- In a T0 topological space `X`, the assignment `x ↦ diracProba x` is a bijection to its |
| 136 | +range in `ProbabilityMeasure X`. -/ |
| 137 | +noncomputable def diracProbaEquiv [T0Space X] : X ≃ range (diracProba (X := X)) where |
| 138 | + toFun := fun x ↦ ⟨diracProba x, by exact mem_range_self x⟩ |
| 139 | + invFun := diracProbaInverse |
| 140 | + left_inv x := by apply diracProbaInverse_eq; rfl |
| 141 | + right_inv μ := Subtype.ext (by simp only [diracProba_diracProbaInverse]) |
| 142 | + |
| 143 | +/-- The composition of `diracProbaEquiv.symm` and `diracProba` is the subtype inclusion. -/ |
| 144 | +lemma diracProba_comp_diracProbaEquiv_symm_eq_val [T0Space X] : |
| 145 | + diracProba ∘ (diracProbaEquiv (X := X)).symm = fun μ ↦ μ.val := by |
| 146 | + funext μ; simp [diracProbaEquiv] |
| 147 | + |
| 148 | +lemma tendsto_diracProbaEquivSymm_iff_tendsto [T0Space X] [CompletelyRegularSpace X] |
| 149 | + {μ : range (diracProba (X := X))} (F : Filter (range (diracProba (X := X)))) : |
| 150 | + Tendsto diracProbaEquiv.symm F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ) := by |
| 151 | + have key := |
| 152 | + tendsto_diracProba_iff_tendsto (F.map diracProbaEquiv.symm) (x := diracProbaEquiv.symm μ) |
| 153 | + rw [← (diracProbaEquiv (X := X)).symm_comp_self, ← tendsto_map'_iff] at key |
| 154 | + simp only [tendsto_map'_iff, map_map, Equiv.self_comp_symm, map_id] at key |
| 155 | + simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val] |
| 156 | + convert tendsto_subtype_rng.symm |
| 157 | + exact apply_rangeSplitting (fun x ↦ diracProba x) μ |
| 158 | + |
| 159 | +/-- In a T0 topological space, `diracProbaEquiv` is continuous. -/ |
| 160 | +lemma continuous_diracProbaEquiv [T0Space X] : |
| 161 | + Continuous (diracProbaEquiv (X := X)) := |
| 162 | + Continuous.subtype_mk continuous_diracProba mem_range_self |
| 163 | + |
| 164 | +/-- In a completely regular T0 topological space, the inverse of `diracProbaEquiv` is continuous. -/ |
| 165 | +lemma continuous_diracProbaEquivSymm [T0Space X] [CompletelyRegularSpace X] : |
| 166 | + Continuous (diracProbaEquiv (X := X)).symm := by |
| 167 | + apply continuous_iff_continuousAt.mpr |
| 168 | + intro μ |
| 169 | + apply continuousAt_of_tendsto_nhds (y := diracProbaInverse μ) |
| 170 | + exact (tendsto_diracProbaEquivSymm_iff_tendsto _).mpr fun _ mem_nhd ↦ mem_nhd |
| 171 | + |
| 172 | +/-- In a completely regular T0 topological space `X`, `diracProbaEquiv` is a homeomorphism to |
| 173 | +its image in `ProbabilityMeasure X`. -/ |
| 174 | +noncomputable def diracProbaHomeomorph [T0Space X] [CompletelyRegularSpace X] |
| 175 | + [MeasurableSpace X] [OpensMeasurableSpace X] : X ≃ₜ range (diracProba (X := X)) := |
| 176 | + @Homeomorph.mk X _ _ _ diracProbaEquiv continuous_diracProbaEquiv continuous_diracProbaEquivSymm |
| 177 | + |
| 178 | +/-- If `X` is a completely regular T0 space with its Borel sigma algebra, then the mapping |
| 179 | +that takes a point `x : X` to the delta-measure `diracProba x` is an embedding |
| 180 | +`X → ProbabilityMeasure X`. -/ |
| 181 | +theorem embedding_diracProba [T0Space X] [CompletelyRegularSpace X] |
| 182 | + [MeasurableSpace X] [OpensMeasurableSpace X] : Embedding (fun (x : X) ↦ diracProba x) := |
| 183 | + embedding_subtype_val.comp diracProbaHomeomorph.embedding |
| 184 | + |
| 185 | +end embed_to_probabilityMeasure |
0 commit comments