chore(MeasureSpace): move dirac and count to new files (#6116)

Mathlib.lean

@@ -2371,6 +2371,8 @@ import Mathlib.MeasureTheory.Measure.AEDisjoint
 import Mathlib.MeasureTheory.Measure.AEMeasurable
 import Mathlib.MeasureTheory.Measure.Complex
 import Mathlib.MeasureTheory.Measure.Content
+import Mathlib.MeasureTheory.Measure.Count
+import Mathlib.MeasureTheory.Measure.Dirac
 import Mathlib.MeasureTheory.Measure.Doubling
 import Mathlib.MeasureTheory.Measure.FiniteMeasure
 import Mathlib.MeasureTheory.Measure.GiryMonad

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Johannes Hölzl
 import Mathlib.Dynamics.Ergodic.MeasurePreserving
 import Mathlib.MeasureTheory.Function.SimpleFunc
 import Mathlib.MeasureTheory.Measure.MutuallySingular
+import Mathlib.MeasureTheory.Measure.Count
 
 #align_import measure_theory.integral.lebesgue from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"
 
@@ -41,42 +42,6 @@ open Classical Topology BigOperators NNReal ENNReal MeasureTheory
 
 namespace MeasureTheory
 
-section MoveThis
-
-variable {m : MeasurableSpace α} {μ ν : Measure α} {f : α → ℝ≥0∞} {s : Set α}
-
--- todo after the port: move to measure_theory/measure/measure_space
-theorem restrict_dirac' (hs : MeasurableSet s) [Decidable (a ∈ s)] :
-    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by
-  ext1 t ht
-  classical
-    simp only [Measure.restrict_apply ht, Measure.dirac_apply' _ (ht.inter hs), Set.indicator_apply,
-      Set.mem_inter_iff, Pi.one_apply]
-    by_cases has : a ∈ s
-    · simp only [has, and_true_iff, if_true]
-      split_ifs with hat
-      · rw [Measure.dirac_apply_of_mem hat]
-      · simp only [Measure.dirac_apply' _ ht, Set.indicator_apply, hat, if_false]
-    · simp only [has, and_false_iff, if_false, Measure.coe_zero, Pi.zero_apply]
-#align measure_theory.restrict_dirac' MeasureTheory.restrict_dirac'
-
--- todo after the port: move to measure_theory/measure/measure_space
-theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
-    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by
-  ext1 t ht
-  classical
-    simp only [Measure.restrict_apply ht, Measure.dirac_apply a, Set.indicator_apply,
-      Set.mem_inter_iff, Pi.one_apply]
-    by_cases has : a ∈ s
-    · simp only [has, and_true_iff, if_true]
-      split_ifs with hat
-      · rw [Measure.dirac_apply_of_mem hat]
-      · simp only [Measure.dirac_apply' _ ht, Set.indicator_apply, hat, if_false]
-    · simp only [has, and_false_iff, if_false, Measure.coe_zero, Pi.zero_apply]
-#align measure_theory.restrict_dirac MeasureTheory.restrict_dirac
-
-end MoveThis
-
 -- mathport name: «expr →ₛ »
 local infixr:25 " →ₛ " => SimpleFunc
 

Mathlib/MeasureTheory/Measure/Count.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import Mathlib.MeasureTheory.Measure.Dirac
+
+/-!
+# Counting measure
+
+In this file we define the counting measure `MeasurTheory.Measure.count`
+as `MeasureTheory.Measure.sum MeasureTheory.Measure.dirac`
+and prove basic properties of this measure.
+-/
+open Set
+open scoped ENNReal BigOperators Classical
+
+variable [MeasurableSpace α] [MeasurableSpace β] {s : Set α}
+
+noncomputable section
+
+namespace MeasureTheory.Measure
+
+/-- Counting measure on any measurable space. -/
+def count : Measure α :=
+  sum dirac
+#align measure_theory.measure.count MeasureTheory.Measure.count
+
+theorem le_count_apply : ∑' _ : s, (1 : ℝ≥0∞) ≤ count s :=
+  calc
+    (∑' _ : s, 1 : ℝ≥0∞) = ∑' i, indicator s 1 i := tsum_subtype s 1
+    _ ≤ ∑' i, dirac i s := (ENNReal.tsum_le_tsum fun _ => le_dirac_apply)
+    _ ≤ count s := le_sum_apply _ _
+#align measure_theory.measure.le_count_apply MeasureTheory.Measure.le_count_apply
+
+theorem count_apply (hs : MeasurableSet s) : count s = ∑' i : s, 1 := by
+  simp only [count, sum_apply, hs, dirac_apply', ← tsum_subtype s (1 : α → ℝ≥0∞), Pi.one_apply]
+#align measure_theory.measure.count_apply MeasureTheory.Measure.count_apply
+
+-- @[simp] -- Porting note: simp can prove this
+theorem count_empty : count (∅ : Set α) = 0 := by rw [count_apply MeasurableSet.empty, tsum_empty]
+#align measure_theory.measure.count_empty MeasureTheory.Measure.count_empty
+
+@[simp]
+theorem count_apply_finset' {s : Finset α} (s_mble : MeasurableSet (s : Set α)) :
+    count (↑s : Set α) = s.card :=
+  calc
+    count (↑s : Set α) = ∑' i : (↑s : Set α), 1 := count_apply s_mble
+    _ = ∑ i in s, 1 := (s.tsum_subtype 1)
+    _ = s.card := by simp
+
+#align measure_theory.measure.count_apply_finset' MeasureTheory.Measure.count_apply_finset'
+
+@[simp]
+theorem count_apply_finset [MeasurableSingletonClass α] (s : Finset α) :
+    count (↑s : Set α) = s.card :=
+  count_apply_finset' s.measurableSet
+#align measure_theory.measure.count_apply_finset MeasureTheory.Measure.count_apply_finset
+
+theorem count_apply_finite' {s : Set α} (s_fin : s.Finite) (s_mble : MeasurableSet s) :
+    count s = s_fin.toFinset.card := by
+  simp [←
+    @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]
+#align measure_theory.measure.count_apply_finite' MeasureTheory.Measure.count_apply_finite'
+
+theorem count_apply_finite [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite) :
+    count s = hs.toFinset.card := by rw [← count_apply_finset, Finite.coe_toFinset]
+#align measure_theory.measure.count_apply_finite MeasureTheory.Measure.count_apply_finite
+
+/-- `count` measure evaluates to infinity at infinite sets. -/
+theorem count_apply_infinite (hs : s.Infinite) : count s = ∞ := by
+  refine' top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => _)
+  rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
+  calc
+    (t.card : ℝ≥0∞) = ∑ i in t, 1 := by simp
+    _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
+    _ ≤ count (t : Set α) := le_count_apply
+    _ ≤ count s := measure_mono ht
+
+#align measure_theory.measure.count_apply_infinite MeasureTheory.Measure.count_apply_infinite
+
+@[simp]
+theorem count_apply_eq_top' (s_mble : MeasurableSet s) : count s = ∞ ↔ s.Infinite := by
+  by_cases hs : s.Finite
+  · simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
+  · change s.Infinite at hs
+    simp [hs, count_apply_infinite]
+#align measure_theory.measure.count_apply_eq_top' MeasureTheory.Measure.count_apply_eq_top'
+
+@[simp]
+theorem count_apply_eq_top [MeasurableSingletonClass α] : count s = ∞ ↔ s.Infinite := by
+  by_cases hs : s.Finite
+  · exact count_apply_eq_top' hs.measurableSet
+  · change s.Infinite at hs
+    simp [hs, count_apply_infinite]
+#align measure_theory.measure.count_apply_eq_top MeasureTheory.Measure.count_apply_eq_top
+
+@[simp]
+theorem count_apply_lt_top' (s_mble : MeasurableSet s) : count s < ∞ ↔ s.Finite :=
+  calc
+    count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top
+    _ ↔ ¬s.Infinite := (not_congr (count_apply_eq_top' s_mble))
+    _ ↔ s.Finite := Classical.not_not
+
+#align measure_theory.measure.count_apply_lt_top' MeasureTheory.Measure.count_apply_lt_top'
+
+@[simp]
+theorem count_apply_lt_top [MeasurableSingletonClass α] : count s < ∞ ↔ s.Finite :=
+  calc
+    count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top
+    _ ↔ ¬s.Infinite := (not_congr count_apply_eq_top)
+    _ ↔ s.Finite := Classical.not_not
+
+#align measure_theory.measure.count_apply_lt_top MeasureTheory.Measure.count_apply_lt_top
+
+theorem empty_of_count_eq_zero' (s_mble : MeasurableSet s) (hsc : count s = 0) : s = ∅ := by
+  have hs : s.Finite := by
+    rw [← count_apply_lt_top' s_mble, hsc]
+    exact WithTop.zero_lt_top
+  simpa [count_apply_finite' hs s_mble] using hsc
+#align measure_theory.measure.empty_of_count_eq_zero' MeasureTheory.Measure.empty_of_count_eq_zero'
+
+theorem empty_of_count_eq_zero [MeasurableSingletonClass α] (hsc : count s = 0) : s = ∅ := by
+  have hs : s.Finite := by
+    rw [← count_apply_lt_top, hsc]
+    exact WithTop.zero_lt_top
+  simpa [count_apply_finite _ hs] using hsc
+#align measure_theory.measure.empty_of_count_eq_zero MeasureTheory.Measure.empty_of_count_eq_zero
+
+@[simp]
+theorem count_eq_zero_iff' (s_mble : MeasurableSet s) : count s = 0 ↔ s = ∅ :=
+  ⟨empty_of_count_eq_zero' s_mble, fun h => h.symm ▸ count_empty⟩
+#align measure_theory.measure.count_eq_zero_iff' MeasureTheory.Measure.count_eq_zero_iff'
+
+@[simp]
+theorem count_eq_zero_iff [MeasurableSingletonClass α] : count s = 0 ↔ s = ∅ :=
+  ⟨empty_of_count_eq_zero, fun h => h.symm ▸ count_empty⟩
+#align measure_theory.measure.count_eq_zero_iff MeasureTheory.Measure.count_eq_zero_iff
+
+theorem count_ne_zero' (hs' : s.Nonempty) (s_mble : MeasurableSet s) : count s ≠ 0 := by
+  rw [Ne.def, count_eq_zero_iff' s_mble]
+  exact hs'.ne_empty
+#align measure_theory.measure.count_ne_zero' MeasureTheory.Measure.count_ne_zero'
+
+theorem count_ne_zero [MeasurableSingletonClass α] (hs' : s.Nonempty) : count s ≠ 0 := by
+  rw [Ne.def, count_eq_zero_iff]
+  exact hs'.ne_empty
+#align measure_theory.measure.count_ne_zero MeasureTheory.Measure.count_ne_zero
+
+@[simp]
+theorem count_singleton' {a : α} (ha : MeasurableSet ({a} : Set α)) : count ({a} : Set α) = 1 := by
+  rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]
+  simp [@toFinset_card _ _ (Set.finite_singleton a).fintype,
+    @Fintype.card_unique _ _ (Set.finite_singleton a).fintype]
+#align measure_theory.measure.count_singleton' MeasureTheory.Measure.count_singleton'
+
+-- @[simp] -- Porting note: simp can prove this
+theorem count_singleton [MeasurableSingletonClass α] (a : α) : count ({a} : Set α) = 1 :=
+  count_singleton' (measurableSet_singleton a)
+#align measure_theory.measure.count_singleton MeasureTheory.Measure.count_singleton
+
+theorem count_injective_image' {f : β → α} (hf : Function.Injective f) {s : Set β}
+    (s_mble : MeasurableSet s) (fs_mble : MeasurableSet (f '' s)) : count (f '' s) = count s := by
+  by_cases hs : s.Finite
+  · lift s to Finset β using hs
+    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
+      s.card_image_of_injective hf]
+    simpa only [Finset.coe_image] using fs_mble
+  · rw [count_apply_infinite hs]
+    rw [← finite_image_iff <| hf.injOn _] at hs
+    rw [count_apply_infinite hs]
+#align measure_theory.measure.count_injective_image' MeasureTheory.Measure.count_injective_image'
+
+theorem count_injective_image [MeasurableSingletonClass α] [MeasurableSingletonClass β] {f : β → α}
+    (hf : Function.Injective f) (s : Set β) : count (f '' s) = count s := by
+  by_cases hs : s.Finite
+  · exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet
+  rw [count_apply_infinite hs]
+  rw [← finite_image_iff <| hf.injOn _] at hs
+  rw [count_apply_infinite hs]
+#align measure_theory.measure.count_injective_image MeasureTheory.Measure.count_injective_image
+
+instance count.isFiniteMeasure [Finite α] [MeasurableSpace α] :
+    IsFiniteMeasure (Measure.count : Measure α) :=
+  ⟨by
+    cases nonempty_fintype α
+    simpa [Measure.count_apply, tsum_fintype] using (ENNReal.nat_ne_top _).lt_top⟩
+#align measure_theory.measure.count.is_finite_measure MeasureTheory.Measure.count.isFiniteMeasure

Mathlib/MeasureTheory/Measure/Dirac.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import Mathlib.MeasureTheory.Measure.MeasureSpace
+/-!
+# Dirac measure
+
+In this file we define the Dirac measure `MeasureTheory.Measure.dirac a`
+and prove some basic facts about it.
+-/
+
+open Function Set
+open scoped ENNReal Classical
+
+noncomputable section
+
+variable [MeasurableSpace α] [MeasurableSpace β] {s : Set α}
+
+namespace MeasureTheory
+
+namespace Measure
+
+/-- The dirac measure. -/
+def dirac (a : α) : Measure α := (OuterMeasure.dirac a).toMeasure (by simp)
+#align measure_theory.measure.dirac MeasureTheory.Measure.dirac
+
+instance : MeasureSpace PUnit :=
+  ⟨dirac PUnit.unit⟩
+
+theorem le_dirac_apply {a} : s.indicator 1 a ≤ dirac a s :=
+  OuterMeasure.dirac_apply a s ▸ le_toMeasure_apply _ _ _
+#align measure_theory.measure.le_dirac_apply MeasureTheory.Measure.le_dirac_apply
+
+@[simp]
+theorem dirac_apply' (a : α) (hs : MeasurableSet s) : dirac a s = s.indicator 1 a :=
+  toMeasure_apply _ _ hs
+#align measure_theory.measure.dirac_apply' MeasureTheory.Measure.dirac_apply'
+
+@[simp]
+theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1 := by
+  have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
+  refine' le_antisymm (this univ trivial ▸ _) (this s h ▸ le_dirac_apply)
+  rw [← dirac_apply' a MeasurableSet.univ]
+  exact measure_mono (subset_univ s)
+#align measure_theory.measure.dirac_apply_of_mem MeasureTheory.Measure.dirac_apply_of_mem
+
+@[simp]
+theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
+    dirac a s = s.indicator 1 a := by
+  by_cases h : a ∈ s; · rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
+  rw [indicator_of_not_mem h, ← nonpos_iff_eq_zero]
+  calc
+    dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
+    _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
+
+#align measure_theory.measure.dirac_apply MeasureTheory.Measure.dirac_apply
+
+theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) :=
+  ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]
+#align measure_theory.measure.map_dirac MeasureTheory.Measure.map_dirac
+
+@[simp]
+theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict {a} = μ {a} • dirac a := by
+  ext1 s hs
+  by_cases ha : a ∈ s
+  · have : s ∩ {a} = {a} := by simpa
+    simp [*]
+  · have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
+    simp [*]
+#align measure_theory.measure.restrict_singleton MeasureTheory.Measure.restrict_singleton
+
+/-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures. -/
+theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β)
+    (hf : Measurable f) : μ.map f = sum fun b : β => μ (f ⁻¹' {b}) • dirac b := by
+  ext1 s hs
+  have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)
+  simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
+    tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]
+#align measure_theory.measure.map_eq_sum MeasureTheory.Measure.map_eq_sum
+
+/-- A measure on a countable type is a sum of Dirac measures. -/
+@[simp]
+theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measure α) :
+    (sum fun a => μ {a} • dirac a) = μ := by simpa using (map_eq_sum μ id measurable_id).symm
+#align measure_theory.measure.sum_smul_dirac MeasureTheory.Measure.sum_smul_dirac
+
+/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
+write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/
+theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α)
+    (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s :=
+  calc
+    (∑' x : α, s.indicator (fun x => μ {x}) x) =
+      Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
+      simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
+        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
+    _ = μ s := by rw [μ.sum_smul_dirac]
+#align measure_theory.measure.tsum_indicator_apply_singleton MeasureTheory.Measure.tsum_indicator_apply_singleton
+
+end Measure
+
+open Measure
+
+theorem mem_ae_dirac_iff {a : α} (hs : MeasurableSet s) : s ∈ (dirac a).ae ↔ a ∈ s := by
+  by_cases a ∈ s <;> simp [mem_ae_iff, dirac_apply', hs.compl, indicator_apply, *]
+#align measure_theory.mem_ae_dirac_iff MeasureTheory.mem_ae_dirac_iff
+
+theorem ae_dirac_iff {a : α} {p : α → Prop} (hp : MeasurableSet { x | p x }) :
+    (∀ᵐ x ∂dirac a, p x) ↔ p a :=
+  mem_ae_dirac_iff hp
+#align measure_theory.ae_dirac_iff MeasureTheory.ae_dirac_iff
+
+@[simp]
+theorem ae_dirac_eq [MeasurableSingletonClass α] (a : α) : (dirac a).ae = pure a := by
+  ext s
+  simp [mem_ae_iff, imp_false]
+#align measure_theory.ae_dirac_eq MeasureTheory.ae_dirac_eq
+
+theorem ae_eq_dirac' [MeasurableSingletonClass β] {a : α} {f : α → β} (hf : Measurable f) :
+    f =ᵐ[dirac a] const α (f a) :=
+  (ae_dirac_iff <| show MeasurableSet (f ⁻¹' {f a}) from hf <| measurableSet_singleton _).2 rfl
+#align measure_theory.ae_eq_dirac' MeasureTheory.ae_eq_dirac'
+
+theorem ae_eq_dirac [MeasurableSingletonClass α] {a : α} (f : α → δ) :
+    f =ᵐ[dirac a] const α (f a) := by simp [Filter.EventuallyEq]
+#align measure_theory.ae_eq_dirac MeasureTheory.ae_eq_dirac
+
+instance Measure.dirac.isProbabilityMeasure [MeasurableSpace α] {x : α} :
+    IsProbabilityMeasure (dirac x) :=
+  ⟨dirac_apply_of_mem <| mem_univ x⟩
+#align measure_theory.measure.dirac.is_probability_measure MeasureTheory.Measure.dirac.isProbabilityMeasure
+
+theorem restrict_dirac' (hs : MeasurableSet s) [Decidable (a ∈ s)] :
+    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by
+  split_ifs with has
+  · apply restrict_eq_self_of_ae_mem
+    rw [ae_dirac_iff] <;> assumption
+  · rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_not_mem has]
+#align measure_theory.restrict_dirac' MeasureTheory.restrict_dirac'
+
+theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
+    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by
+  split_ifs with has
+  · apply restrict_eq_self_of_ae_mem
+    rwa [ae_dirac_eq]
+  · rw [restrict_eq_zero, dirac_apply, indicator_of_not_mem has]
+#align measure_theory.restrict_dirac MeasureTheory.restrict_dirac