Documentation

Mathlib.MeasureTheory.Measure.Count

Counting measure #

In this file we define the counting measure MeasureTheory.Measure.count as MeasureTheory.Measure.sum MeasureTheory.Measure.dirac and prove basic properties of this measure.

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

Counting measure on any measurable space.

Equations
Instances For
    source
    @[simp]
    theorem MeasureTheory.Measure.count_ne_zero'' {α : Type u_1} [MeasurableSpace α] [Nonempty α] :
    count ≠ 0
    source
    theorem MeasureTheory.Measure.le_count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} :
    ∑' (x : ↑s), 1 ≤ count s
    source
    theorem MeasureTheory.Measure.count_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) :
    count s = ↑s.encard
    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_finset' {α : Type u_1} [MeasurableSpace α] {s : Finset α} (hs : MeasurableSet ↑s) :
    count ↑s = ↑s.card
    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_finset {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) :
    count ↑s = ↑s.card
    source
    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
    source
    theorem MeasureTheory.Measure.count_apply_finite {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite) :
    count s = ↑hs.toFinset.card
    source
    theorem MeasureTheory.Measure.count_apply_infinite {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : s.Infinite) :
    count s = ⊤

    count measure evaluates to infinity at infinite sets.

    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_eq_top' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_mble : MeasurableSet s) :
    count s = ⊤ ↔ s.Infinite
    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_eq_top {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] :
    count s = ⊤ ↔ s.Infinite
    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_lt_top' {α : Type u_1} [MeasurableSpace α] {s : Set α} (s_mble : MeasurableSet s) :
    count s < ⊤ ↔ s.Finite
    source
    @[simp]
    theorem MeasureTheory.Measure.count_apply_lt_top {α : Type u_1} [MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α] :
    count s < ⊤ ↔ s.Finite
    source
    @[simp]
    theorem MeasureTheory.Measure.count_eq_zero_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} :
    count s = 0 ↔ s = ∅
    source
    theorem MeasureTheory.Measure.count_ne_zero_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} :
    count s ≠ 0 ↔ s.Nonempty
    source
    theorem MeasureTheory.Measure.count_ne_zero {α : Type u_1} [MeasurableSpace α] {s : Set α} :
    s.Nonempty → count s ≠ 0

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

    source
    @[simp]
    theorem MeasureTheory.Measure.ae_count_iff {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :
    (∀ᵐ (x : α) ∂count, p x) ↔ ∀ (x : α), p x
    source
    @[simp]
    theorem MeasureTheory.Measure.count_singleton' {α : Type u_1} [MeasurableSpace α] {a : α} (ha : MeasurableSet {a}) :
    count {a} = 1
    source
    theorem MeasureTheory.Measure.count_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
    count {a} = 1
    source
    @[simp]
    theorem MeasureTheory.count_real_singleton' {α : Type u_1} [MeasurableSpace α] {a : α} (ha : MeasurableSet {a}) :
    Measure.count.real {a} = 1
    source
    theorem MeasureTheory.count_real_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
    Measure.count.real {a} = 1
    source
    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)) :
    count (f '' s) = count s
    source
    theorem MeasureTheory.Measure.count_injective_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {f : β → α} (hf : Function.Injective f) (s : Set β) :
    count (f '' s) = count s
    source
    instance MeasureTheory.Measure.count.instSigmaFinite {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] :
    SigmaFinite count
    source
    instance MeasureTheory.Measure.count.isFiniteMeasure {α : Type u_1} [MeasurableSpace α] [Finite α] :
    IsFiniteMeasure count
    source
    @[simp]
    theorem MeasureTheory.Measure.count_univ {α : Type u_1} [MeasurableSpace α] :
    count Set.univ = ↑(ENat.card α)
    source
    @[simp]
    theorem MeasureTheory.Measure.count_real_univ {α : Type u_1} [MeasurableSpace α] :
    count.real Set.univ = ↑(Nat.card α)
    source
    instance MeasureTheory.Measure.neZero_count {α : Type u_1} [MeasurableSpace α] [Nonempty α] :
    NeZero count
    source
    theorem Subsingleton.count_eq_dirac {α : Type u_1} [MeasurableSpace α] [Subsingleton α] (i : α) :
    MeasureTheory.Measure.count = MeasureTheory.Measure.dirac i
    source
    theorem Unique.count_eq_dirac {α : Type u_1} [MeasurableSpace α] [Unique α] :
    MeasureTheory.Measure.count = MeasureTheory.Measure.dirac default
    source
    theorem Function.Injective.map_count_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Injective f) (h2f : Measurable f) :
    MeasureTheory.Measure.map f MeasureTheory.Measure.count ≤ MeasureTheory.Measure.count