# Measure spaces

Given a measurable space `α`

, a measure on `α`

is a function that sends measurable sets to the
extended nonnegative reals that satisfies the following conditions:

`μ ∅ = 0`

;`μ`

is countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the measure of the individual sets.

Every measure can be canonically extended to an outer measure, so that it assigns values to all subsets, not just the measurable subsets. On the other hand, a measure that is countably additive on measurable sets can be restricted to measurable sets to obtain a measure. In this file a measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

Measures on `α`

form a complete lattice, and are closed under scalar multiplication with `ennreal`

.

We introduce the following typeclasses for measures:

`probability_measure μ`

:`μ univ = 1`

;`finite_measure μ`

:`μ univ < ⊤`

;`sigma_finite μ`

: there exists a countable collection of measurable sets that cover`univ`

where`μ`

is finite;`locally_finite_measure μ`

:`∀ x, ∃ s ∈ 𝓝 x, μ s < ⊤`

;`has_no_atoms μ`

:`∀ x, μ {x} = 0`

; possibly should be redefined as`∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s`

.

Given a measure, the null sets are the sets where `μ s = 0`

, where `μ`

denotes the corresponding
outer measure (so `s`

might not be measurable). We can then define the completion of `μ`

as the
measure on the least `σ`

-algebra that also contains all null sets, by defining the measure to be `0`

on the null sets.

## Main statements

`completion`

is the completion of a measure to all null measurable sets.`measure.of_measurable`

and`outer_measure.to_measure`

are two important ways to define a measure.

## Implementation notes

Given `μ : measure α`

, `μ s`

is the value of the *outer measure* applied to `s`

.
This conveniently allows us to apply the measure to sets without proving that they are measurable.
We get countable subadditivity for all sets, but only countable additivity for measurable sets.

You often don't want to define a measure via its constructor. Two ways that are sometimes more convenient:

`measure.of_measurable`

is a way to define a measure by only giving its value on measurable sets and proving the properties (1) and (2) mentioned above.`outer_measure.to_measure`

is a way of obtaining a measure from an outer measure by showing that all measurable sets in the measurable space are Carathéodory measurable.

To prove that two measures are equal, there are multiple options:

`ext`

: two measures are equal if they are equal on all measurable sets.`ext_of_generate_from_of_Union`

: two measures are equal if they are equal on a π-system generating the measurable sets, if the π-system contains a spanning increasing sequence of sets where the measures take finite value (in particular the measures are σ-finite). This is a special case of the more general`ext_of_generate_from_of_cover`

`ext_of_generate_finite`

: two finite measures are equal if they are equal on a π-system generating the measurable sets. This is a special case of`ext_of_generate_from_of_Union`

using`C ∪ {univ}`

, but is easier to work with.

A `measure_space`

is a class that is a measurable space with a canonical measure.
The measure is denoted `volume`

.

## References

- https://en.wikipedia.org/wiki/Measure_(mathematics)
- https://en.wikipedia.org/wiki/Complete_measure
- https://en.wikipedia.org/wiki/Almost_everywhere

## Tags

measure, almost everywhere, measure space, completion, null set, null measurable set

- to_outer_measure : measure_theory.outer_measure α
- m_Union : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), is_measurable (f i)) → pairwise (disjoint on f) → c.to_outer_measure.measure_of (⋃ (i : ℕ), f i) = ∑' (i : ℕ), c.to_outer_measure.measure_of (f i)
- trimmed : c.to_outer_measure.trim = c.to_outer_measure

A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

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.

## Equations

- measure_theory.measure.has_coe_to_fun = {F := λ (_x : measure_theory.measure α), set α → ennreal, coe := λ (m : measure_theory.measure α), ⇑(m.to_outer_measure)}

### General facts about measures

Obtain a measure by giving a countably additive function that sends `∅`

to `0`

.

## Equations

- measure_theory.measure.of_measurable m m0 mU = {to_outer_measure := {measure_of := (measure_theory.induced_outer_measure m is_measurable.empty m0).measure_of, empty := _, mono := _, Union_nat := _}, m_Union := _, trimmed := _}

A variant of `measure_eq_infi`

which has a single `infi`

. This is useful when applying a
lemma next that only works for non-empty infima, in which case you can use
`nonempty_measurable_superset`

.

A measurable set `t ⊇ s`

such that `μ t = μ s`

.

## Equations

If `s`

is a countable set, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`

.

If `s`

is a `finset`

, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`

.

Pigeonhole principle for measure spaces: if `∑' i, μ (s i) > μ univ`

, then
one of the intersections `s i ∩ s j`

is not empty.

Pigeonhole principle for measure spaces: if `s`

is a `finset`

and
`∑ i in s, μ (t i) > μ univ`

, then one of the intersections `t i ∩ t j`

is not empty.

Continuity from below: the measure of the union of a directed sequence of measurable sets is the supremum of the measures.

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the infimum of the measures.

Continuity from below: the measure of the union of an increasing sequence of measurable sets is the limit of the measures.

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.

One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that ∑ μ sᵢ exists, then the limit superior of the sᵢ is a null set.

Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.

## Equations

- m.to_measure h = measure_theory.measure.of_measurable (λ (s : set α) (_x : is_measurable s), ⇑m s) _ _

### The `ennreal`

-module of measures

## Equations

- measure_theory.measure.has_zero = {zero := {to_outer_measure := 0, m_Union := _, trimmed := _}}

## Equations

- measure_theory.measure.has_add = {add := λ (μ₁ μ₂ : measure_theory.measure α), {to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure, m_Union := _, trimmed := _}}

## Equations

- measure_theory.measure.has_scalar = {smul := λ (c : ennreal) (μ : measure_theory.measure α), {to_outer_measure := c • μ.to_outer_measure, m_Union := _, trimmed := _}}

### The complete lattice of measures

## Equations

- measure_theory.measure.partial_order = {le := λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), is_measurable s → ⇑m₁ s ≤ ⇑m₂ s, lt := preorder.lt._default (λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), is_measurable s → ⇑m₁ s ≤ ⇑m₂ s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

## Equations

- measure_theory.measure.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_top := _, bot := 0, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

### Pushforward and pullback

Lift a linear map between `outer_measure`

spaces such that for each measure `μ`

every measurable
set is caratheodory-measurable w.r.t. `f μ`

to a linear map between `measure`

spaces.

## Equations

- measure_theory.measure.lift_linear f hf = {to_fun := λ (μ : measure_theory.measure α), (⇑f μ.to_outer_measure).to_measure _, map_add' := _, map_smul' := _}

The pushforward of a measure. It is defined to be `0`

if `f`

is not a measurable function.

## Equations

- measure_theory.measure.map f = dite (measurable f) (λ (hf : measurable f), measure_theory.measure.lift_linear (measure_theory.outer_measure.map f) _) (λ (hf : ¬measurable f), 0)

We can evaluate the pushforward on measurable sets. For non-measurable sets, see
`measure_theory.measure.le_map_apply`

and `measurable_equiv.map_apply`

.

Even if `s`

is not measurable, we can bound `map f μ s`

from below.
See also `measurable_equiv.map_apply`

.

Pullback of a `measure`

. If `f`

sends each `measurable`

set to a `measurable`

set, then for each
measurable set `s`

we have `comap f μ s = μ (f '' s)`

.

## Equations

- measure_theory.measure.comap f = dite (function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s)) (λ (hf : function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s)), measure_theory.measure.lift_linear (measure_theory.outer_measure.comap f) _) (λ (hf : ¬(function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s))), 0)

### Restricting a measure

Restrict a measure `μ`

to a set `s`

as an `ennreal`

-linear map.

Restrict a measure `μ`

to a set `s`

.

## Equations

- μ.restrict s = ⇑(measure_theory.measure.restrictₗ s) μ

Restriction of a measure to a subset is monotone both in set and in measure.

If two measures agree on all measurable subsets of `s`

and `t`

, then they agree on all
measurable subsets of `s ∪ t`

.

This lemma shows that `restrict`

and `to_outer_measure`

commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures.

This lemma shows that `Inf`

and `restrict`

commute for measures.

### Extensionality results

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `Union`

).

**Alias** of `ext_iff_of_Union_eq_univ`

.

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `bUnion`

).

**Alias** of `ext_iff_of_bUnion_eq_univ`

.

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `sUnion`

).

**Alias** of `ext_iff_of_sUnion_eq_univ`

.

Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on a increasing spanning sequence of sets in the π-system.
This lemma is formulated using `sUnion`

.

Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on a increasing spanning sequence of sets in the π-system.
This lemma is formulated using `Union`

.
`finite_spanning_sets_in.ext`

is a reformulation of this lemma.

The dirac measure.

## Equations

Sum of an indexed family of measures.

## Equations

- measure_theory.measure.sum f = (measure_theory.outer_measure.sum (λ (i : ι), (f i).to_outer_measure)).to_measure _

Counting measure on any measurable space.

`count`

measure evaluates to infinity at infinite sets.

### The almost everywhere filter

The “almost everywhere” filter of co-null sets.

The filter of sets `s`

such that `sᶜ`

has finite measure.

A version of the Borel-Cantelli lemma: if `sᵢ`

is a sequence of measurable sets such that
`∑ μ sᵢ`

exists, then for almost all `x`

, `x`

does not belong to almost all `sᵢ`

.

If `s ⊆ t`

modulo a set of measure `0`

, then `μ s ≤ μ t`

.

**Alias** of `measure_mono_ae`

.

If two sets are equal modulo a set of measure zero, then `μ s = μ t`

.

A measure `μ`

is called a probability measure if `μ univ = 1`

.

A measure `μ`

is called finite if `μ univ < ⊤`

.

Measure `μ`

*has no atoms* if the measure of each singleton is zero.

NB: Wikipedia assumes that for any measurable set `s`

with positive `μ`

-measure,
there exists a measurable `t ⊆ s`

such that `0 < μ t < μ s`

. While this implies `μ {x} = 0`

,
the converse is not true.

`le_of_add_le_add_left`

is normally applicable to `ordered_cancel_add_comm_monoid`

,
but it holds for measures with the additional assumption that μ is finite.

A measure is called finite at filter `f`

if it is finite at some set `s ∈ f`

.
Equivalently, it is eventually finite at `s`

in `f.lift' powerset`

.

- set : ℕ → set α
- set_mem : ∀ (i : ℕ), c.set i ∈ C
- finite : ∀ (i : ℕ), ⇑μ (c.set i) < ⊤
- spanning : (⋃ (i : ℕ), c.set i) = set.univ

`μ`

has finite spanning sets in `C`

if there is a countable sequence of sets in `C`

that have
finite measures. This structure is a type, which is useful if we want to record extra properties
about the sets, such as that they are monotone.
`sigma_finite`

is defined in terms of this: `μ`

is σ-finite if there exists a sequence of
finite spanning sets in the collection of all measurable sets.

A measure `μ`

is called σ-finite if there is a countable collection of sets
`{ A i | i ∈ ℕ }`

such that `μ (A i) < ⊤`

and `⋃ i, A i = s`

.

## Equations

- measure_theory.sigma_finite μ = nonempty (μ.finite_spanning_sets_in {s : set α | is_measurable s})

## Instances

- measure_theory.finite_measure.to_sigma_finite
- measure_theory.sigma_finite_of_locally_finite
- measure_theory.restrict.sigma_finite
- measure_theory.sum.sigma_finite
- measure_theory.add.sigma_finite
- measure_theory.measure.prod.sigma_finite
- measure_theory.measure.haar_measure.measure_theory.sigma_finite
- measure_theory.measure.sigma_finite_tprod

If `μ`

is σ-finite it has finite spanning sets in the collection of all measurable sets.

## Equations

A noncomputable way to get a monotone collection of sets that span `univ`

and have finite
measure using `classical.some`

. This definition satisfies monotonicity in addition to all other
properties in `sigma_finite`

.

## Equations

If `μ`

has finite spanning sets in `C`

and `C ⊆ D`

then `μ`

has finite spanning sets in `D`

.

If `μ`

has finite spanning sets in the collection of measurable sets `C`

, then `μ`

is σ-finite.

An extensionality for measures. It is `ext_of_generate_from_of_Union`

formulated in terms of
`finite_spanning_sets_in`

.

Every finite measure is σ-finite.

- finite_at_nhds : ∀ (x : α), μ.finite_at_filter (𝓝 x)

A measure is called locally finite if it is finite in some neighborhood of each point.

If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.

Two finite measures are equal if they are equal on the π-system generating the σ-algebra
(and `univ`

).

**Alias** of `inf_ae_iff`

.

### Subtraction of measures

The measure `μ - ν`

is defined to be the least measure `τ`

such that `μ ≤ τ + ν`

.
It is the equivalent of `(μ - ν) ⊔ 0`

if `μ`

and `ν`

were signed measures.
Compare with `ennreal.has_sub`

.
Specifically, note that if you have `α = {1,2}`

, and `μ {1} = 2`

, `μ {2} = 0`

, and
`ν {2} = 2`

, `ν {1} = 0`

, then `(μ - ν) {1, 2} = 2`

. However, if `μ ≤ ν`

, and
`ν univ ≠ ⊤`

, then `(μ - ν) + ν = μ`

.

## Equations

- measure_theory.measure.has_sub = {sub := λ (μ ν : measure_theory.measure α), Inf {τ : measure_theory.measure α | μ ≤ τ + ν}}

This application lemma only works in special circumstances. Given knowledge of
when `μ ≤ ν`

and `ν ≤ μ`

, a more general application lemma can be written.

Interactions of measurable equivalences and measures

If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).

A measure is complete if every null set is also measurable.
A null set is a subset of a measurable set with measure `0`

.
Since every measure is defined as a special case of an outer measure, we can more simply state
that a set `s`

is null if `μ s = 0`

.

## Equations

- μ.is_complete = ∀ (s : set α), ⇑μ s = 0 → is_measurable s

## Instances

A set is null measurable if it is the union of a null set and a measurable set.

## Equations

- is_null_measurable μ s = ∃ (t z : set α), s = t ∪ z ∧ is_measurable t ∧ ⇑μ z = 0

The measurable space of all null measurable sets.

## Equations

- null_measurable μ = {is_measurable' := is_null_measurable μ, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}

Given a measure we can complete it to a (complete) measure on all null measurable sets.

## Equations

- completion μ = {to_outer_measure := μ.to_outer_measure, m_Union := _, trimmed := _}

- to_measurable_space : measurable_space α
- volume : measure_theory.measure α

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

.

The tactic `exact volume`

, to be used in optional (`auto_param`

) arguments.

# Almost everywhere measurable functions

A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function. We define this property, called `ae_measurable f μ`

, and discuss several of its properties
that are analogous to properties of measurable functions.

A function is almost everywhere measurable if it coincides almost everywhere with a measurable function.

## Equations

- ae_measurable f μ = ∃ (g : α → β), measurable g ∧ f =ᵐ[μ] g

Given an almost everywhere measurable function `f`

, associate to it a measurable function
that coincides with it almost everywhere. `f`

is explicit in the definition to make sure that
it shows in pretty-printing.

## Equations

- ae_measurable.mk f h = classical.some h