# 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`

,`ℝ≥0∞`

.

## Main statements #

`is_open.measurable_set`

,`is_closed.measurable_set`

: 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`

;`ae_measurable.add`

: similar dot notation for almost everywhere measurable functions;`measurable.ennreal*`

: special cases for arithmetic operations on`ℝ≥0∞`

.

`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.

## Instances of this typeclass

- order_dual.borel_space
- is_R_or_C.borel_space
- subtype.borel_space
- pi.borel_space
- prod.borel_space
- empty.borel_space
- unit.borel_space
- bool.borel_space
- nat.borel_space
- int.borel_space
- rat.borel_space
- real.borel_space
- nnreal.borel_space
- ennreal.borel_space
- ereal.borel_space
- complex.borel_space
- add_circle.borel_space
- continuous_linear_map.borel_space

The behaviour of `borelize α`

depends on the existing assumptions on `α`

.

- if
`α`

is a topological space with instances`[measurable_space α] [borel_space α]`

, then`borelize α`

replaces the former instance by`borel α`

; - otherwise,
`borelize α`

adds instances`borel α : measurable_space α`

and`⟨rfl⟩ : borel_space α`

.

Finally, `borelize [α, β, γ]`

runs `borelize α, borelize β, borelize γ`

.

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 : measurable_set s`

.

Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If
`α`

is a conditionally complete linear order with no top element,
`measure_theory.measure..ext_of_Ico`

is an extensionality lemma with weaker assumptions on `μ`

and
`ν`

.

Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If
`α`

is a conditionally complete linear order with no top element,
`measure_theory.measure..ext_of_Ioc`

is an extensionality lemma with weaker assumptions on `μ`

and
`ν`

.

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

A continuous function from an `opens_measurable_space`

to a `borel_space`

is measurable.

A continuous function from an `opens_measurable_space`

to a `borel_space`

is ae-measurable.

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it 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 := _}

If a set is a right-neighborhood of all of its points, then it is measurable.

`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

## Equations

## Equations

## Equations

One can cut out `ℝ≥0∞`

into the sets `{0}`

, `Ico (t^n) (t^(n+1))`

for `n : ℤ`

and `{∞}`

. This
gives a way to compute the measure of a set in terms of sets on which a given function `f`

does not
fluctuate by more than `t`

.

If a set has a closed thickening with finite measure, then the measure of its `r`

-closed
thickenings converges to the measure of its closure as `r`

tends to `0`

.

If a closed set has a closed thickening with finite measure, then the measure of its `r`

-closed
thickenings converges to its measure as `r`

tends to `0`

.

Given a compact set in a proper space, the measure of its `r`

-closed thickenings converges to
its measure as `r`

tends to `0`

.

The intervals `(-(n + 1), (n + 1))`

form a finite spanning sets in the set of open intervals
with rational endpoints for a locally finite measure `μ`

on `ℝ`

.

The set of finite `ℝ≥0∞`

numbers is `measurable_equiv`

to `ℝ≥0`

.

`ℝ≥0∞`

is `measurable_equiv`

to `ℝ≥0 ⊕ unit`

.

## Equations

- ennreal.ennreal_equiv_sum = {to_equiv := {to_fun := (equiv.option_equiv_sum_punit nnreal).to_fun, inv_fun := (equiv.option_equiv_sum_punit nnreal).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: `ℝ≥0∞`

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

The set of finite `ereal`

numbers is `measurable_equiv`

to `ℝ`

.

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

valued functions is measurable.

A sequential limit of measurable `ℝ≥0∞`

valued functions is measurable.

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

valued functions is measurable.

A sequential limit of measurable `ℝ≥0`

valued functions is measurable.

A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is measurable.

A sequential limit of measurable functions valued in a (pseudo) metrizable space is measurable.