Measure

“A Measure on (X : set α): subset of X → non-negative real number”

/--
Let X be a set and Σ a σ-algebra over X.

A function μ from Σ to the extended real number line is called a measure

if it satisfies the following properties:
-/
class measure (μ : Σ → ℝ≥0∞) :=
(non_neg : ∀ E ∈ Σ, μ E ≥ 0)
(null_empty_set : μ ∅ = 0)
(count_add :   ∀ (E : ℕ → set α) [∀ i, E i ⊆ Σ],
               ∀ i j, disjoint (E i) (E j),
                 μ(⋃ i, E i) = ∑ i, μ(E i))
)

“The pair (X, Σ) is called a Measurable space, the members of Σ are called measurable sets.”

“A triple (X, Σ, μ) is called a Measure space. A Probability measure is a measure with total measure one – i.e. μ(X) = 1. A Probability space is a Measure space with a Probability measure.”

instances of measure: distances, length, area, volume, mass, probability, etc.

“Measures can be generalized to assume negative values, as with electrical charge.”

“One would like to assign a size to every subset of X, but in many natural settings, this is not possible.

For example, the axiom of choice implies that when the size under consideration is the ordinary notion of length for subsets of the real line, then there exist sets for which no size exists, for example, the Vitali sets.

For this reason, one considers instead a smaller collection of privileged subsets of X. Measurable sets. Closed under operations that one would expect for measurable sets, that is, the complement of a measurable set is a measurable set and the countable union of measurable sets is a measurable set.

Non-empty collections of sets with these properties are called ∑-algebras.”

• Instances of Measure:

  • Counting measure: μ(S) = card S;

  • The Lebesgue measure on ℝ is a complete translation-invariant measure on a ∑-algebra containing the intervals in ℝ such that μ([0, 1]) = 1; and every other measure with these properties extends Lebesgue measure.

  • Circular angle measure is invariant under rotation, and hyperbolic angle measure is invariant under squeeze mapping.

  • Haar measure for a locally compact topological group is a generalization of the Lebesgue measure (and also of counting measure and circular angle measure) and has similar uniqueness properties.

  • Every probability space gives rise to a measure which takes the value 1 on the whole space (and therefore takes all its values in the unit interval [0, 1]). Such a measure is called a probability measure.

  • The Dirac measure δa (cf. Dirac delta function) is given by δa(S) = χS(a), where χS is the indicator function of S. The measure of a set is 1 if it contains the point a and 0 otherwise

  • Positive operator valued measure (POVM);

theorem monotonicity (μ : Σ → ℝ≥0∞) [measure μ] :
∀ E₁ E₂,
measurable E₁ ∧ measurable E₂ → 
E₁ ⊆ E₂ → 
μ E₁ ≤ μ E₂ := sorry

References

• Wikipedia: Measure;