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>

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

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