Documentation

Mathlib.MeasureTheory.Measure.Count

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.

theorem MeasureTheory.Measure.le_count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} :
∑' (x : s), 1 count s
theorem MeasureTheory.Measure.count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) :
count s = ∑' (x : s), 1
@[simp]
theorem MeasureTheory.Measure.count_apply_finset' {α : Type u_1} [MeasurableSpace α] {s : Finset α} (s_mble : MeasurableSet s) :
count s = s.card
theorem MeasureTheory.Measure.count_apply_finite' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_fin : s.Finite) (s_mble : MeasurableSet s) :
count s = s_fin.toFinset.card

count measure evaluates to infinity at infinite sets.

@[simp]
@[simp]
theorem MeasureTheory.Measure.count_ne_zero {α : Type u_1} [MeasurableSpace α] {s : Set α} :
s.Nonemptycount s 0

Alias of the reverse direction of MeasureTheory.Measure.count_ne_zero_iff.

@[deprecated MeasureTheory.Measure.count_eq_zero_iff (since := "2024-11-20")]

Alias of the forward direction of MeasureTheory.Measure.count_eq_zero_iff.

@[deprecated MeasureTheory.Measure.empty_of_count_eq_zero (since := "2024-11-20")]

Alias of the forward direction of MeasureTheory.Measure.count_eq_zero_iff.


Alias of the forward direction of MeasureTheory.Measure.count_eq_zero_iff.

@[deprecated MeasureTheory.Measure.count_eq_zero_iff (since := "2024-11-20")]

Alias of MeasureTheory.Measure.count_eq_zero_iff.

@[deprecated MeasureTheory.Measure.count_ne_zero (since := "2024-11-20")]
theorem MeasureTheory.Measure.count_ne_zero' {α : Type u_1} [MeasurableSpace α] {s : Set α} :
s.Nonemptycount s 0

Alias of the reverse direction of MeasureTheory.Measure.count_ne_zero_iff.


Alias of the reverse direction of MeasureTheory.Measure.count_ne_zero_iff.

@[simp]
theorem MeasureTheory.Measure.count_injective_image' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : Function.Injective f) {s : Set β} (s_mble : MeasurableSet s) (fs_mble : MeasurableSet (f '' s)) :