# Spaces where indicators of closed sets have decreasing approximations by continuous functions #

In this file we define a typeclass `HasOuterApproxClosed`

for topological spaces in which indicator
functions of closed sets have sequences of bounded continuous functions approximating them from
above. All pseudo-emetrizable spaces have this property, see `instHasOuterApproxClosed`

.

In spaces with the `HasOuterApproxClosed`

property, finite Borel measures are uniquely characterized
by the integrals of bounded continuous functions. Also weak convergence of finite measures and
convergence in distribution for random variables behave somewhat well in spaces with this property.

## Main definitions #

`HasOuterApproxClosed`

: the typeclass for topological spaces in which indicator functions of closed sets have sequences of bounded continuous functions approximating them.`IsClosed.apprSeq`

: a (non-constructive) choice of an approximating sequence to the indicator function of a closed set.

## Main results #

`instHasOuterApproxClosed`

: Any pseudo-emetrizable space has the property`HasOuterApproxClosed`

.`tendsto_lintegral_apprSeq`

: The integrals of the approximating functions to the indicator of a closed set tend to the measure of the set.`ext_of_forall_lintegral_eq_of_IsFiniteMeasure`

: Two finite measures are equal if the integrals of all bounded continuous functions with respect to both agree.

A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes:

- the functions tend to a limit along a countably generated filter;
- the limit is in the almost everywhere sense;
- boundedness holds almost everywhere;
- integration is
`MeasureTheory.lintegral`

, i.e., the functions and their integrals are`ℝ≥0∞`

-valued.

If bounded continuous functions tend to the indicator of a measurable set and are uniformly bounded, then their integrals against a finite measure tend to the measure of the set. This formulation assumes:

- the functions tend to a limit along a countably generated filter;
- the limit is in the almost everywhere sense;
- boundedness holds almost everywhere.

If a sequence of bounded continuous functions tends to the indicator of a measurable set and the functions are uniformly bounded, then their integrals against a finite measure tend to the measure of the set.

A similar result with more general assumptions is
`MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator`

.

The integrals of thickened indicators of a closed set against a finite measure tend to the measure of the closed set if the thickening radii tend to zero.

A type class for topological spaces in which the indicator functions of closed sets can be approximated pointwise from above by a sequence of bounded continuous functions.

## Instances

A sequence of continuous functions `X → [0,1]`

tending to the indicator of a closed set.

## Equations

- hF.apprSeq = ⋯.choose

## Instances For

The measure of a closed set is at most the integral of any function in a decreasing approximating sequence to the indicator of the set.

The integrals along a decreasing approximating sequence to the indicator of a closed set tend to the measure of the closed set.

## Equations

- ⋯ = ⋯

Two finite measures give equal values to all closed sets if the integrals of all bounded continuous functions with respect to the two measures agree.

Two finite Borel measures are equal if the integrals of all bounded continuous functions with respect to both agree.