# Borel (measurable) space

## Main definitions

`borel α`

: the least`σ`

-algebra that contains all open sets;`class borel_space`

: a space with`topological_space`

and`measurable_space`

structures such that`‹measurable_space α› = borel α`

;`class opens_measurable_space`

: a space with`topological_space`

and`measurable_space`

structures such that all open sets are measurable; equivalently,`borel α ≤ ‹measurable_space α›`

.`borel_space`

instances on`empty`

,`unit`

,`bool`

,`nat`

,`int`

,`rat`

;`measurable`

and`borel_space`

instances on`ℝ`

,`ℝ≥0`

,`ennreal`

.- A measure is
`regular`

if it is finite on compact sets, inner regular and outer regular.

## Main statements

`is_open.is_measurable`

,`is_closed.is_measurable`

: open and closed sets are measurable;`continuous.measurable`

: a continuous function is measurable;`continuous.measurable2`

: if`f : α → β`

and`g : α → γ`

are measurable and`op : β × γ → δ`

is continuous, then`λ x, op (f x, g y)`

is measurable;`measurable.add`

etc : dot notation for arithmetic operations on`measurable`

predicates, and similarly for`dist`

and`edist`

;`measurable.ennreal*`

: special cases for arithmetic operations on`ennreal`

s.

`measurable_space`

structure generated by `topological_space`

.

## Equations

- borel α = measurable_space.generate_from {s : set α | is_open s}

A space with `measurable_space`

and `topological_space`

structures such that
all open sets are measurable.

A space with `measurable_space`

and `topological_space`

structures such that
the `σ`

-algebra of measurable sets is exactly the `σ`

-algebra generated by open sets.

In a `borel_space`

all open sets are measurable.

If `s`

is a measurable set, then `𝓝[s] a`

is a measurably generated filter for
each `a`

. This cannot be an `instance`

because it depends on a non-instance `hs : is_measurable s`

.

A continuous function from an `opens_measurable_space`

to a `borel_space`

is measurable.

A homeomorphism between two Borel spaces is a measurable equivalence.

## Equations

- h.to_measurable_equiv = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

A variant of `measurable.mul`

that uses `*`

on functions

`liminf`

over a general filter is measurable. See `measurable_liminf`

for the version over `ℕ`

.

`limsup`

over a general filter is measurable. See `measurable_limsup`

for the version over `ℕ`

.

`liminf`

over `ℕ`

is measurable. See `measurable_liminf'`

for a version with a general filter.

`limsup`

over `ℕ`

is measurable. See `measurable_limsup'`

for a version with a general filter.

Convert a `homeomorph`

to a `measurable_equiv`

.

## Equations

- homemorph.to_measurable_equiv h = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

## Equations

## Equations

## Equations

## Equations

The set of finite `ennreal`

numbers is `measurable_equiv`

to `ℝ≥0`

.

`ennreal`

is `measurable_equiv`

to `ℝ≥0 ⊕ unit`

.

## Equations

- ennreal.ennreal_equiv_sum = {to_equiv := {to_fun := (equiv.option_equiv_sum_punit ℝ≥0).to_fun, inv_fun := (equiv.option_equiv_sum_punit ℝ≥0).inv_fun, left_inv := ennreal.ennreal_equiv_sum._proof_1, right_inv := ennreal.ennreal_equiv_sum._proof_2}, measurable_to_fun := ennreal.ennreal_equiv_sum._proof_3, measurable_inv_fun := ennreal.ennreal_equiv_sum._proof_4}

note: `ennreal`

can probably be generalized in a future version of this lemma.

A limit (over a general filter) of measurable `ℝ≥0`

valued functions is measurable.
The assumption `hs`

can be dropped using `filter.is_countably_generated.has_antimono_basis`

, but we
don't need that case yet.

A sequential limit of measurable `ℝ≥0`

valued functions is measurable.

A limit (over a general filter) of measurable functions valued in a metric space is measurable.
The assumption `hs`

can be dropped using `filter.is_countably_generated.has_antimono_basis`

, but we
don't need that case yet.

A sequential limit of measurable functions valued in a metric space is measurable.

- lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → ⇑μ K < ⊤
- outer_regular : ∀ ⦃A : set α⦄, is_measurable A → (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), ⇑μ U) ≤ ⇑μ A
- inner_regular : ∀ ⦃U : set α⦄, is_open U → (⇑μ U ≤ ⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), ⇑μ K)

A measure `μ`

is regular if

- it is finite on all compact sets;
- it is outer regular:
`μ(A) = inf { μ(U) | A ⊆ U open }`

for`A`

measurable; - it is inner regular:
`μ(U) = sup { μ(K) | K ⊆ U compact }`

for`U`

open.