MeasureTheory.Measure.count_apply
theorem MeasureTheory.Measure.count_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α},
MeasurableSet s → ↑↑MeasureTheory.Measure.count s = ∑' (i : ↑s), 1
This theorem states that for any type `α` and any measurable set `s` of `α` (in the given measurable space), the counting measure of `s` is equivalent to the sum of `1` for each element `i` in `s`. In other words, the counting measure of a measurable set is simply the number of elements in the set.
More concisely: For any measurable set `s` in a given measurable space, the counting measure of `s` equals the cardinality of `s`.
|
MeasureTheory.Measure.count_apply_infinite
theorem MeasureTheory.Measure.count_apply_infinite :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, s.Infinite → ↑↑MeasureTheory.Measure.count s = ⊤ := by
sorry
This theorem states that for any type `α` that is a measurable space, if `s` is an infinite set of `α`, then the count measure of `s` is infinity. In other words, when applying the counting measure to an infinite set in any measurable space, the result is always infinity. This encodes the intuitive notion that counting an infinite set would go on forever, yielding an infinite measure.
More concisely: For any measurable space `α`, the counting measure of an infinite subset of `α` is infinity.
|
MeasureTheory.Measure.empty_of_count_eq_zero
theorem MeasureTheory.Measure.empty_of_count_eq_zero :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [inst_1 : MeasurableSingletonClass α],
↑↑MeasureTheory.Measure.count s = 0 → s = ∅
This theorem states that for any type `α` that has a measurable space structure, and any set `s` of `α` that has a measurable singleton class structure, if the counting measure of the set `s` is equal to zero, then the set `s` must be the empty set. Essentially, the theorem is saying that if there are no measurable elements in the set (hence, the measure is zero), the set must be empty.
More concisely: If `α` is a type with a measurable space structure, `s` is a subset of `α` with a measurable singleton class structure, and the counting measure of `s` is zero, then `s` is the empty set.
|
MeasureTheory.Measure.count_apply_finite'
theorem MeasureTheory.Measure.count_apply_finite' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} (s_fin : s.Finite),
MeasurableSet s → ↑↑MeasureTheory.Measure.count s = ↑s_fin.toFinset.card
The theorem `MeasureTheory.Measure.count_apply_finite'` states that for any type `α` equipped with a measure space structure, and for any finite and measurable set `s` of `α`, the counting measure of `s` is equal to the cardinality of the `Finset` that represents `s`. In other words, the counting measure simply counts the number of elements in the finite set `s`, which is exactly the same as the number of elements in the corresponding `Finset`.
More concisely: For any finite and measurable set `s` in a measure space `α`, the counting measure of `s` equals its cardinality.
|
MeasureTheory.Measure.count_apply_finite
theorem MeasureTheory.Measure.count_apply_finite :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (s : Set α) (hs : s.Finite),
↑↑MeasureTheory.Measure.count s = ↑hs.toFinset.card
The theorem `MeasureTheory.Measure.count_apply_finite` states that for any set `s` of type `α`, in a measurable space where singletons are measurable, if `s` is finite then the counting measure of `s` is equal to the cardinality of the finite set represented by `s`. This simply means that the counting measure, which counts the number of elements in the set, will indeed return the actual number of elements in the finite set.
More concisely: In a measurable space where singletons are measurable, the counting measure of a finite set equals its cardinality.
|
MeasureTheory.Measure.count_apply_lt_top
theorem MeasureTheory.Measure.count_apply_lt_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [inst_1 : MeasurableSingletonClass α],
↑↑MeasureTheory.Measure.count s < ⊤ ↔ s.Finite
This theorem states that for any set `s` of a certain type `α` in a measurable space, the count measure (which assigns the cardinality of the set as its measure) is less than infinity if and only if the set `s` is finite. This is to say, the theorem establishes a connection between the finiteness of a set and its count measure being less than infinity. The `MeasurableSingletonClass α` is an assumption that ensures singletons of `α` are measurable, allowing the use of the counting measure.
More concisely: For a set `s` of type `α` in a measurable space, the count measure of `s` is less than infinity if and only if `s` is finite. (Assuming `MeasurableSingletonClass α`)
|
MeasureTheory.Measure.count_empty
theorem MeasureTheory.Measure.count_empty :
∀ {α : Type u_1} [inst : MeasurableSpace α], ↑↑MeasureTheory.Measure.count ∅ = 0
This theorem states that for any type `α` endowed with a measurable space structure, the counting measure of the empty set is equal to zero. In simpler words, it states that there are no elements to count in an empty set, hence its measure or size is zero.
More concisely: For any measurable space `(α, Σ)`, the measure of the empty set `∅` is 0, i.e., `∫ₗ(1 : Σ → Prop) d(measure ∅) = 0`.
|
MeasureTheory.Measure.count_apply_finset'
theorem MeasureTheory.Measure.count_apply_finset' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Finset α},
MeasurableSet ↑s → ↑↑MeasureTheory.Measure.count ↑s = ↑s.card
This theorem states that for any finite set `s` in a measurable space `α`, if the set `s` is measurable, then applying the counting measure to `s` is equivalent to finding the cardinality (or number of elements) of `s`. In other words, the counting measure of a measurable finite set is simply its size.
More concisely: For any finite measurable set `s` in a measurable space, the counting measure of `s` equals its cardinality.
|