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.

def MeasureTheory.Measure.count {α : Type u_1} [MeasurableSpace α] : MeasureTheory.Measure α

Counting measure on any measurable space.

Equations

• MeasureTheory.Measure.count = MeasureTheory.Measure.sum MeasureTheory.Measure.dirac

Instances For

• MeasureTheory.Measure.count.isFiniteMeasure

@[simp]

theorem MeasureTheory.Measure.count_ne_zero'' {α : Type u_1} [MeasurableSpace α] [Nonempty α] : MeasureTheory.Measure.count ≠ 0

theorem MeasureTheory.Measure.le_count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} : ∑' (x : ↑s), 1 ≤ MeasureTheory.Measure.count s

theorem MeasureTheory.Measure.count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.count s = ∑' (i : ↑s), 1

theorem MeasureTheory.Measure.count_empty {α : Type u_1} [MeasurableSpace α] : MeasureTheory.Measure.count ∅ = 0

@[simp]

theorem MeasureTheory.Measure.count_apply_finset' {α : Type u_1} [MeasurableSpace α] {s : Finset α} (s_mble : MeasurableSet ↑s) : MeasureTheory.Measure.count ↑s = ↑s.card

@[simp]

theorem MeasureTheory.Measure.count_apply_finset {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) : MeasureTheory.Measure.count ↑s = ↑s.card

theorem MeasureTheory.Measure.count_apply_finite' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_fin : s.Finite) (s_mble : MeasurableSet s) : MeasureTheory.Measure.count s = ↑s_fin.toFinset.card

theorem MeasureTheory.Measure.count_apply_finite {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite) : MeasureTheory.Measure.count s = ↑hs.toFinset.card

theorem MeasureTheory.Measure.count_apply_infinite {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : s.Infinite) : MeasureTheory.Measure.count s = ⊤

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) : MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite

@[simp]

theorem MeasureTheory.Measure.count_apply_eq_top {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] : MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite

@[simp]

theorem MeasureTheory.Measure.count_apply_lt_top' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_mble : MeasurableSet s) : MeasureTheory.Measure.count s < ⊤ ↔ s.Finite

@[simp]

theorem MeasureTheory.Measure.count_apply_lt_top {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] : MeasureTheory.Measure.count s < ⊤ ↔ s.Finite

theorem MeasureTheory.Measure.empty_of_count_eq_zero' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_mble : MeasurableSet s) (hsc : MeasureTheory.Measure.count s = 0) : s = ∅

theorem MeasureTheory.Measure.empty_of_count_eq_zero {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] (hsc : MeasureTheory.Measure.count s = 0) : s = ∅

@[simp]

theorem MeasureTheory.Measure.count_eq_zero_iff' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_mble : MeasurableSet s) : MeasureTheory.Measure.count s = 0 ↔ s = ∅

@[simp]

theorem MeasureTheory.Measure.count_eq_zero_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] : MeasureTheory.Measure.count s = 0 ↔ s = ∅

theorem MeasureTheory.Measure.count_ne_zero' {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs' : s.Nonempty) (s_mble : MeasurableSet s) : MeasureTheory.Measure.count s ≠ 0

theorem MeasureTheory.Measure.count_ne_zero {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] (hs' : s.Nonempty) : MeasureTheory.Measure.count s ≠ 0

@[simp]

theorem MeasureTheory.Measure.count_singleton' {α : Type u_1} [MeasurableSpace α] {a : α} (ha : MeasurableSet {a}) : MeasureTheory.Measure.count {a} = 1

theorem MeasureTheory.Measure.count_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : MeasureTheory.Measure.count {a} = 1

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)) : MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s

theorem MeasureTheory.Measure.count_injective_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {f : β → α} (hf : Function.Injective f) (s : Set β) : MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s

instance MeasureTheory.Measure.count.isFiniteMeasure {α : Type u_1} [MeasurableSpace α] [Finite α] : MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.count

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.Measure.count_univ {α : Type u_1} [MeasurableSpace α] [Fintype α] : MeasureTheory.Measure.count Set.univ = ↑(Fintype.card α)