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.
Counting measure on any measurable space.
Instances For
@[simp]
theorem
MeasureTheory.Measure.count_apply
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(hs : MeasurableSet s)
:
@[deprecated MeasureTheory.measure_empty (since := "2025-02-06")]
@[simp]
theorem
MeasureTheory.Measure.count_apply_finset'
{α : Type u_1}
[MeasurableSpace α]
{s : Finset α}
(hs : MeasurableSet ↑s)
:
@[simp]
theorem
MeasureTheory.Measure.count_apply_finset
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(s : Finset α)
:
theorem
MeasureTheory.Measure.count_apply_finite'
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(s_fin : s.Finite)
(s_mble : MeasurableSet s)
:
theorem
MeasureTheory.Measure.count_apply_finite
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(s : Set α)
(hs : s.Finite)
:
theorem
MeasureTheory.Measure.count_apply_infinite
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(hs : s.Infinite)
:
count
measure evaluates to infinity at infinite sets.
@[simp]
theorem
MeasureTheory.Measure.count_apply_eq_top'
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(s_mble : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.count_apply_eq_top
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
[MeasurableSingletonClass α]
:
@[simp]
theorem
MeasureTheory.Measure.count_apply_lt_top'
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(s_mble : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.count_apply_lt_top
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
[MeasurableSingletonClass α]
:
@[simp]
Alias of the reverse direction of MeasureTheory.Measure.count_ne_zero_iff
.
@[simp]
@[simp]
theorem
MeasureTheory.Measure.count_singleton'
{α : Type u_1}
[MeasurableSpace α]
{a : α}
(ha : MeasurableSet {a})
:
theorem
MeasureTheory.Measure.count_singleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
:
@[simp]
theorem
MeasureTheory.count_real_singleton'
{α : Type u_1}
[MeasurableSpace α]
{a : α}
(ha : MeasurableSet {a})
:
theorem
MeasureTheory.count_real_singleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
:
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))
:
theorem
MeasureTheory.Measure.count_injective_image
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
{f : β → α}
(hf : Function.Injective f)
(s : Set β)
:
instance
MeasureTheory.Measure.count.instSigmaFinite
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Countable α]
:
instance
MeasureTheory.Measure.count.isFiniteMeasure
{α : Type u_1}
[MeasurableSpace α]
[Finite α]
:
@[simp]