From a128cd995f9117c3a933d37b295d7a6b89a348a0 Mon Sep 17 00:00:00 2001 From: kkytola Date: Sun, 3 Sep 2023 11:06:39 +0000 Subject: [PATCH] feat: push-forwards of finite measures and probability measures (#6551) Add push-forwards of finite measures and probability measures, and prove that push-forwards under continuous functions are continuous (w.r.t. the topologies of weak convergence of measures). Besides being a natural addition to the API, this should enable simple proofs of, for example, continuity of some parametric distributions (multi-dimensional gaussians, exponential distribution, ...) with respect to their parameters. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> --- .../MeasureTheory/Measure/FiniteMeasure.lean | 111 ++++++++++++++++-- .../Measure/ProbabilityMeasure.lean | 74 +++++++++++- 2 files changed, 168 insertions(+), 17 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index 31019cddd14b2..2207800503928 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -22,11 +22,16 @@ measure is continuous. ## Main definitions The main definitions are - * the type `MeasureTheory.FiniteMeasure Ω` with the topology of weak convergence; - * `MeasureTheory.FiniteMeasure.toWeakDualBCNN : FiniteMeasure Ω → (WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0))` - allowing to interpret a finite measure as a continuous linear functional on the space of + * `MeasureTheory.FiniteMeasure Ω`: The type of finite measures on `Ω` with the topology of weak + convergence of measures. + * `MeasureTheory.FiniteMeasure.toWeakDualBCNN : FiniteMeasure Ω → (WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0))`: + Interpret a finite measure as a continuous linear functional on the space of bounded continuous nonnegative functions on `Ω`. This is used for the definition of the topology of weak convergence. + * `MeasureTheory.FiniteMeasure.map`: The push-forward `f* μ` of a finite measure `μ` on `Ω` + along a measurable function `f : Ω → Ω'`. + * `MeasureTheory.FiniteMeasure.mapClm`: The push-forward along a given continuous `f : Ω → Ω'` + as a continuous linear map `f* : FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω'`. ## Main results @@ -39,6 +44,8 @@ The main definitions are of weak convergence of measures. A similar characterization by the convergence of integrals (in the `MeasureTheory.lintegral` sense) of all bounded continuous nonnegative functions is `MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto`. + * `MeasureTheory.FiniteMeasure.continuous_map`: For a continuous function `f : Ω → Ω'`, the + push-forward of finite measures `f* : FiniteMeasure Ω → FiniteMeasure Ω'` is continuous. ## Implementation notes @@ -764,12 +771,92 @@ theorem tendsto_iff_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : exact Tendsto.sub tends_pos tends_neg #align measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto -end FiniteMeasureConvergenceByBoundedContinuousFunctions - --- section -end FiniteMeasure - --- namespace -end MeasureTheory - --- namespace +end FiniteMeasureConvergenceByBoundedContinuousFunctions -- section + +section map + +variable {Ω Ω' : Type _} [MeasurableSpace Ω] [MeasurableSpace Ω'] + +/-- The push-forward of a finite measure by a function between measurable spaces. -/ +noncomputable def map (ν : FiniteMeasure Ω) (f : Ω → Ω') : FiniteMeasure Ω' := + ⟨(ν : Measure Ω).map f, by + constructor + by_cases f_aemble : AEMeasurable f ν + · rw [Measure.map_apply_of_aemeasurable f_aemble MeasurableSet.univ] + exact measure_lt_top (↑ν) (f ⁻¹' univ) + · simp [Measure.map, f_aemble]⟩ + +/-- Note that this is an equality of elements of `ℝ≥0∞`. See also +`MeasureTheory.FiniteMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/ +lemma map_apply' (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) + {A : Set Ω'} (A_mble : MeasurableSet A) : + (ν.map f : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) := + Measure.map_apply_of_aemeasurable f_aemble A_mble + +lemma map_apply_of_aemeasurable (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) + {A : Set Ω'} (A_mble : MeasurableSet A) : + ν.map f A = ν (f ⁻¹' A) := by + have := ν.map_apply' f_aemble A_mble + exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr this + +@[simp] lemma map_apply (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_mble : Measurable f) + {A : Set Ω'} (A_mble : MeasurableSet A) : + ν.map f A = ν (f ⁻¹' A) := + map_apply_of_aemeasurable ν f_mble.aemeasurable A_mble + +@[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω) : + (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f := by + ext s s_mble + simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_add] + +@[simp] lemma map_smul {f : Ω → Ω'} (f_mble : Measurable f) (c : ℝ≥0) (ν : FiniteMeasure Ω) : + (c • ν).map f = c • (ν.map f) := by + ext s s_mble + simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_smul] + +/-- The push-forward of a finite measure by a function between measurable spaces as a linear map. -/ +noncomputable def mapHom {f : Ω → Ω'} (f_mble : Measurable f) : + FiniteMeasure Ω →ₗ[ℝ≥0] FiniteMeasure Ω' where + toFun := fun ν ↦ ν.map f + map_add' := map_add f_mble + map_smul' := map_smul f_mble + +variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω] +variable [TopologicalSpace Ω'] [BorelSpace Ω'] + +/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then +(weak) convergence of `FiniteMeasure`s on `X` implies (weak) convergence of the push-forwards +of these measures by `f`. -/ +lemma tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} + (νs : ι → FiniteMeasure Ω) (ν : FiniteMeasure Ω) (lim : Tendsto νs L (𝓝 ν)) + {f : Ω → Ω'} (f_cont : Continuous f) : + Tendsto (fun i ↦ (νs i).map f) L (𝓝 (ν.map f)) := by + rw [FiniteMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢ + intro g + convert lim (g.compContinuous ⟨f, f_cont⟩) <;> + · simp only [map, compContinuous_apply, ContinuousMap.coe_mk] + refine lintegral_map ?_ f_cont.measurable + exact (ENNReal.continuous_coe.comp g.continuous).measurable + +/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then +the push-forward of finite measures `f* : FiniteMeasure X → FiniteMeasure Y` is continuous +(in the topologies of weak convergence of measures). -/ +lemma continuous_map {f : Ω → Ω'} (f_cont : Continuous f) : + Continuous (fun ν ↦ FiniteMeasure.map ν f) := by + rw [continuous_iff_continuousAt] + exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont + +/-- The push-forward of a finite measure by a continuous function between Borel spaces as +a continuous linear map. -/ +noncomputable def mapClm {f : Ω → Ω'} (f_cont : Continuous f) : + FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω' where + toFun := fun ν ↦ ν.map f + map_add' := map_add f_cont.measurable + map_smul' := map_smul f_cont.measurable + cont := continuous_map f_cont + +end map -- section + +end FiniteMeasure -- namespace + +end MeasureTheory -- namespace diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean index e23ed5f2d2fad..dec1fdb89ee15 100644 --- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean @@ -28,6 +28,8 @@ The main definitions are a finite measure; * `MeasureTheory.FiniteMeasure.normalize`: Normalize a finite measure to a probability measure (returns junk for the zero measure). + * `MeasureTheory.ProbabilityMeasure.map`: The push-forward `f* μ` of a probability measure + `μ` on `Ω` along a measurable function `f : Ω → Ω'`. ## Main results @@ -41,6 +43,9 @@ The main definitions are * `MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto`: The convergence of finite measures to a nonzero limit is characterized by the convergence of the probability-normalized versions and of the total masses. + * `MeasureTheory.ProbabilityMeasure.continuous_map`: For a continuous function `f : Ω → Ω'`, the + push-forward of probability measures `f* : ProbabilityMeasure Ω → ProbabilityMeasure Ω'` is + continuous. TODO: * Probability measures form a convex space. @@ -491,10 +496,69 @@ theorem tendsto_normalize_iff_tendsto {γ : Type*} {F : Filter γ} {μs : γ → refine' ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩ #align measure_theory.finite_measure.tendsto_normalize_iff_tendsto MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto -end FiniteMeasure +end FiniteMeasure --namespace ---namespace -end NormalizeFiniteMeasure +end NormalizeFiniteMeasure -- section --- section -end MeasureTheory +section map + +variable {Ω Ω' : Type _} [MeasurableSpace Ω] [MeasurableSpace Ω'] + +namespace ProbabilityMeasure + +/-- The push-forward of a probability measure by a measurable function. -/ +noncomputable def map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) : + ProbabilityMeasure Ω' := + ⟨(ν : Measure Ω).map f, + ⟨by simp only [Measure.map_apply_of_aemeasurable f_aemble MeasurableSet.univ, + preimage_univ, measure_univ]⟩⟩ + +/-- Note that this is an equality of elements of `ℝ≥0∞`. See also +`MeasureTheory.ProbabilityMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/ +lemma map_apply' (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) + {A : Set Ω'} (A_mble : MeasurableSet A) : + (ν.map f_aemble : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) := + Measure.map_apply_of_aemeasurable f_aemble A_mble + +lemma map_apply_of_aemeasurable (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} + (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) : + (ν.map f_aemble) A = ν (f ⁻¹' A) := by + have := ν.map_apply' f_aemble A_mble + exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr this + +@[simp] lemma map_apply (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) + {A : Set Ω'} (A_mble : MeasurableSet A) : + (ν.map f_aemble) A = ν (f ⁻¹' A) := + map_apply_of_aemeasurable ν f_aemble A_mble + +variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω] +variable [TopologicalSpace Ω'] [BorelSpace Ω'] + +/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then +convergence (in distribution) of `ProbabilityMeasure`s on `X` implies convergence (in +distribution) of the push-forwards of these measures by `f`. -/ +lemma tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} + (νs : ι → ProbabilityMeasure Ω) (ν : ProbabilityMeasure Ω) (lim : Tendsto νs L (𝓝 ν)) + {f : Ω → Ω'} (f_cont : Continuous f) : + Tendsto (fun i ↦ (νs i).map f_cont.measurable.aemeasurable) L + (𝓝 (ν.map f_cont.measurable.aemeasurable)) := by + rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢ + intro g + convert lim (g.compContinuous ⟨f, f_cont⟩) <;> + · simp only [map, compContinuous_apply, ContinuousMap.coe_mk] + refine lintegral_map ?_ f_cont.measurable + exact (ENNReal.continuous_coe.comp g.continuous).measurable + +/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then +the push-forward of probability measures `f* : ProbabilityMeasure X → ProbabilityMeasure Y` +is continuous (in the topologies of convergence in distribution). -/ +lemma continuous_map {f : Ω → Ω'} (f_cont : Continuous f) : + Continuous (fun ν ↦ ProbabilityMeasure.map ν f_cont.measurable.aemeasurable) := by + rw [continuous_iff_continuousAt] + exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont + +end ProbabilityMeasure -- namespace + +end map -- section + +end MeasureTheory -- namespace