feat : refactor IsUniform through uniformMeasure (#10456)

Refactor the definitions and proofs of IsUniform through the new `uniformMeasure`, which abstracts away from the need of a random variable and probability space.

A future PR can refactor the PMF parts in terms of a `uniformMeasure`.

This was #10141, which was split into a small PR to move the results (merged) and this one.

Author: JADekker

Mathlib/Probability/ConditionalProbability.lean

@@ -78,15 +78,52 @@ end Definitions
 @[inherit_doc] scoped notation μ "[" s "|" t "]" => ProbabilityTheory.cond μ t s
 @[inherit_doc] scoped notation:60 μ "[|" t "]" => ProbabilityTheory.cond μ t
 
-/-- The conditional probability measure of any finite measure on any set of positive measure
+/-- The conditional probability measure of any measure on any set of finite positive measure
 is a probability measure. -/
-theorem cond_isProbabilityMeasure [IsFiniteMeasure μ] (hcs : μ s ≠ 0) :
+theorem cond_isProbabilityMeasure_of_finite (hcs : μ s ≠ 0) (hs : μ s ≠ ∞) :
     IsProbabilityMeasure (μ[|s]) :=
   ⟨by
-    rw [cond, Measure.smul_apply, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
-    exact ENNReal.inv_mul_cancel hcs (measure_ne_top _ s)⟩
+    unfold ProbabilityTheory.cond
+    simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply,
+      MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul]
+    exact ENNReal.inv_mul_cancel hcs hs⟩
+
+/-- The conditional probability measure of any finite measure on any set of positive measure
+is a probability measure. -/
+theorem cond_isProbabilityMeasure [IsFiniteMeasure μ] (hcs : μ s ≠ 0) :
+    IsProbabilityMeasure (μ[|s]) := cond_isProbabilityMeasure_of_finite μ hcs (measure_ne_top μ s)
 #align probability_theory.cond_is_probability_measure ProbabilityTheory.cond_isProbabilityMeasure
 
+instance cond_isFiniteMeasure :
+    IsFiniteMeasure (μ[|s]) where
+  measure_univ_lt_top := by
+    unfold ProbabilityTheory.cond
+    have : (μ s)⁻¹ * μ s < ⊤ := by
+      have : (μ s)⁻¹ * μ s ≤ 1 := by
+        apply ENNReal.le_inv_iff_mul_le.mp
+        rfl
+      exact lt_of_le_of_lt this ENNReal.one_lt_top
+    simp_all only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
+      le_refl, Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply,
+      smul_eq_mul]
+
+theorem cond_toMeasurable_eq :
+    μ[|(toMeasurable μ s)] = μ[|s] := by
+  unfold cond
+  by_cases hnt : μ s = ∞
+  · simp [hnt]
+  · simp [Measure.restrict_toMeasurable hnt]
+
+theorem cond_absolutelyContinuous :
+    μ[|s] ≪ μ := by
+  intro t ht
+  unfold ProbabilityTheory.cond
+  rw [Measure.smul_apply, smul_eq_mul]
+  apply mul_eq_zero.mpr
+  refine Or.inr (le_antisymm ?_ (zero_le _))
+  exact ht ▸ Measure.restrict_apply_le s t
+
+
 section Bayes
 
 @[simp]
@@ -103,6 +140,9 @@ theorem cond_apply (hms : MeasurableSet s) (t : Set Ω) : μ[t|s] = (μ s)⁻¹
   rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
 #align probability_theory.cond_apply ProbabilityTheory.cond_apply
 
+ theorem cond_apply' {t : Set Ω} (hA : MeasurableSet t) : μ[t|s] = (μ s)⁻¹ * μ (s ∩ t) := by
+   rw [cond, Measure.smul_apply, Measure.restrict_apply hA, Set.inter_comm, smul_eq_mul]
+
 theorem cond_inter_self (hms : MeasurableSet s) (t : Set Ω) : μ[s ∩ t|s] = μ[t|s] := by
   rw [cond_apply _ hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply _ hms]
 #align probability_theory.cond_inter_self ProbabilityTheory.cond_inter_self

Mathlib/Probability/Distributions/Uniform.lean

@@ -5,6 +5,7 @@ Authors: Josha Dekker, Devon Tuma, Kexing Ying
 -/
 import Mathlib.Probability.Notation
 import Mathlib.Probability.Density
+import Mathlib.Probability.ConditionalProbability
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 /-!
@@ -15,11 +16,16 @@ This file defines two related notions of uniform distributions, which will be un
 
 Defines the uniform distribution for any set with finite measure.
 
+## Main definitions
+* `IsUniform X s ℙ μ` : A random variable `X` has uniform distribution on `s` under `ℙ` if the
+  push-forward measure agrees with the rescaled restricted measure `μ`.
+
 # Uniform probability mass functions
 
 This file defines a number of uniform `PMF` distributions from various inputs,
   uniformly drawing from the corresponding object.
 
+## Main definitions
 `PMF.uniformOfFinset` gives each element in the set equal probability,
   with `0` probability for elements not in the set.
 
@@ -28,35 +34,38 @@ This file defines a number of uniform `PMF` distributions from various inputs,
 
 `PMF.ofMultiset` draws randomly from the given `Multiset`, treating duplicate values as distinct.
   Each probability is given by the count of the element divided by the size of the `Multiset`
+
+# To Do:
+* Refactor the `PMF` definitions to come from a `uniformMeasure` on a `Finset`/`Fintype`/`Multiset`.
 -/
 
 open scoped Classical MeasureTheory BigOperators NNReal ENNReal
 
-open TopologicalSpace MeasureTheory.Measure
+open TopologicalSpace MeasureTheory.Measure PMF
+
+noncomputable section
 
 namespace MeasureTheory
 
 variable {E : Type*} [MeasurableSpace E] {m : Measure E} {μ : Measure E}
-variable {Ω : Type*} {_ : MeasurableSpace Ω} {ℙ : Measure Ω}
 
+namespace pdf
 
-section
-
-/-! **Uniform Distribution based on a measure** -/
+variable {Ω : Type*}
 
-namespace pdf
+variable {_ : MeasurableSpace Ω} {ℙ : Measure Ω}
 
 /-- A random variable `X` has uniform distribution on `s` if its push-forward measure is
 `(μ s)⁻¹ • μ.restrict s`. -/
-def IsUniform (X : Ω → E) (support : Set E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :=
-  map X ℙ = (μ support)⁻¹ • μ.restrict support
+def IsUniform (X : Ω → E) (s : Set E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :=
+  map X ℙ = ProbabilityTheory.cond μ s
 #align measure_theory.pdf.is_uniform MeasureTheory.pdf.IsUniform
 
 namespace IsUniform
 
 theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
     (hu : IsUniform X s ℙ μ) : AEMeasurable X ℙ := by
-  dsimp [IsUniform] at hu
+  dsimp [IsUniform, ProbabilityTheory.cond] at hu
   by_contra h
   rw [map_of_not_aemeasurable h] at hu
   apply zero_ne_one' ℝ≥0∞
@@ -66,17 +75,14 @@ theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s 
       Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]
 
 theorem absolutelyContinuous {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : map X ℙ ≪ μ := by
-  intro t ht
-  rw [hu, smul_apply, smul_eq_mul]
-  apply mul_eq_zero.mpr
-  refine Or.inr (le_antisymm ?_ (zero_le _))
-  exact ht ▸ restrict_apply_le s t
+  rw [hu]
+  exact ProbabilityTheory.cond_absolutelyContinuous μ
 
 theorem measure_preimage {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
     (hu : IsUniform X s ℙ μ) {A : Set E} (hA : MeasurableSet A) :
     ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s := by
-  rw [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, smul_apply, restrict_apply hA,
-    ENNReal.div_eq_inv_mul, smul_eq_mul, Set.inter_comm]
+   rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
+    ENNReal.div_eq_inv_mul.symm]
 #align measure_theory.pdf.is_uniform.measure_preimage MeasureTheory.pdf.IsUniform.measure_preimage
 
 theorem isProbabilityMeasure {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
@@ -89,12 +95,13 @@ theorem isProbabilityMeasure {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt
 
 theorem toMeasurable_iff {X : Ω → E} {s : Set E} :
     IsUniform X (toMeasurable μ s) ℙ μ ↔ IsUniform X s ℙ μ := by
-  by_cases hnt : μ s = ∞
-  · simp [IsUniform, hnt]
-  · simp [IsUniform, restrict_toMeasurable hnt]
+  unfold IsUniform
+  rw [ProbabilityTheory.cond_toMeasurable_eq]
 
 protected theorem toMeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) :
-    IsUniform X (toMeasurable μ s) ℙ μ := toMeasurable_iff.2 hu
+    IsUniform X (toMeasurable μ s) ℙ μ := by
+  unfold IsUniform at *
+  rwa [ProbabilityTheory.cond_toMeasurable_eq]
 
 theorem hasPDF {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
     (hu : IsUniform X s ℙ μ) : HasPDF X ℙ μ := by
@@ -103,14 +110,16 @@ theorem hasPDF {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞
     (measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s)
   rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
     withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable]
+  rfl
 #align measure_theory.pdf.is_uniform.has_pdf MeasureTheory.pdf.IsUniform.hasPDF
 
 theorem pdf_eq_zero_of_measure_eq_zero_or_top {X : Ω → E} {s : Set E}
     (hu : IsUniform X s ℙ μ) (hμs : μ s = 0 ∨ μ s = ∞) : pdf X ℙ μ =ᵐ[μ] 0 := by
   rcases hμs with H|H
-  · simp only [IsUniform, H, ENNReal.inv_zero, restrict_eq_zero.mpr H, smul_zero] at hu
+  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H,
+    smul_zero] at hu
     simp [pdf, hu]
-  · simp only [IsUniform, H, ENNReal.inv_top, zero_smul] at hu
+  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu
     simp [pdf, hu]
 
 theorem pdf_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s)
@@ -124,7 +133,9 @@ theorem pdf_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s)
   have : HasPDF X ℙ μ := hasPDF hns hnt hu
   have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu
   apply (eq_of_map_eq_withDensity _ _).mp
-  · rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one]
+  · rw [hu, withDensity_indicator hms,
+    withDensity_smul _ measurable_one, withDensity_one]
+    rfl
   · exact (measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms
 
 theorem pdf_toReal_ae_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s)
@@ -163,7 +174,9 @@ theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) :
 `(λ s)⁻¹ * ∫ x in s, x ∂λ` where `λ` is the Lebesgue measure. -/
 theorem integral_eq (huX : IsUniform X s ℙ) :
     ∫ x, X x ∂ℙ = (volume s)⁻¹.toReal * ∫ x in s, x := by
-  rw [← smul_eq_mul, ← integral_smul_measure, ← huX]
+  rw [← smul_eq_mul, ← integral_smul_measure]
+  dsimp only [IsUniform, ProbabilityTheory.cond] at huX
+  rw [← huX]
   by_cases hX : AEMeasurable X ℙ
   · exact (integral_map hX aestronglyMeasurable_id).symm
   · rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]
@@ -172,9 +185,33 @@ theorem integral_eq (huX : IsUniform X s ℙ) :
 
 end IsUniform
 
-end pdf
+variable {X : Ω → E}
+
+lemma IsUniform.cond {s : Set E} :
+    IsUniform (id : E → E) s (ProbabilityTheory.cond μ s) μ := by
+  unfold IsUniform
+  rw [Measure.map_id]
+
+/-- The density of the uniform measure on a set with respect to itself. This allows us to abstract
+away the choice of random variable and probability space. -/
+def uniformPDF (s : Set E) (x : E) (μ : Measure E := by volume_tac) : ℝ≥0∞ :=
+  s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) x
 
-end
+/-- Check that indeed any uniform random variable has the uniformPDF. -/
+lemma uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X s ℙ μ) :
+    (fun x ↦ uniformPDF s x μ) =ᵐ[μ] pdf X ℙ μ := by
+  unfold uniformPDF
+  exact Filter.EventuallyEq.trans (pdf.IsUniform.pdf_eq hs hu).symm (ae_eq_refl _)
+
+/-- Alternative way of writing the uniformPDF. -/
+lemma uniformPDF_ite {s : Set E} {x : E} :
+    uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0 := by
+  unfold uniformPDF
+  unfold Set.indicator
+  rename_i inst x_1
+  simp_all only [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one]
+
+end pdf
 
 end MeasureTheory