# 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

- order_dual.borel_space
- is_R_or_C.borel_space
- subtype.borel_space
- pi.borel_space_fintype_encodable
- pi.borel_space_fintype
- 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
- continuous_linear_map.borel_space
- circle.borel_space

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.

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 := _}

`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

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 ℝ≥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: `ℝ≥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 functions valued in a metric space is measurable.
The assumption `hs`

can be dropped using `filter.is_countably_generated.has_antitone_basis`

, but we
don't need that case yet.

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