measure_theory.measure'

Measure projection which is ∞ for non-measurable sets.

measure' is mainly used to derive the outer measure, for the main measure projection.

measure_theory.outer_measure'

outer measure of a measure

measure_theory.measure.has_coe_to_fun

Measure projections for a measure space.

For measurable sets this returns the measure assigned by the measure_of field in measure. But we can extend this to all sets, but using the outer measure. This gives us monotonicity and subadditivity for all sets.

measure_theory.measure.dirac

The dirac measure.

measure_theory.measure.sum

Sum of an indexed family of measures.

measure_theory.measure.count

Counting measure on any measurable space.

measure_theory.measure.a_e

The "almost everywhere" filter of co-null sets.

measure_theory.measure_space

A measure space is a measurable space equipped with a measure, referred to as volume.

measure_theory.all_ae

∀ₘ a:α, p a states that the property p is almost everywhere true in the measure space associated with α. This means that the measure of the complementary of p is 0.

In a probability measure, the measure of p is 1, when p is measurable.