# Vitali-Carathéodory theorem #

Vitali-Carathéodory theorem asserts the following. Consider an integrable function `f : α → ℝ`

on
a space with a regular measure. Then there exists a function `g : α → EReal`

such that `f x < g x`

everywhere, `g`

is lower semicontinuous, and the integral of `g`

is arbitrarily close to that of
`f`

. This theorem is proved in this file, as `exists_lt_lower_semicontinuous_integral_lt`

.

Symmetrically, there exists `g < f`

which is upper semicontinuous, with integral arbitrarily close
to that of `f`

. It follows from the previous statement applied to `-f`

. It is formalized under
the name `exists_upper_semicontinuous_lt_integral_gt`

.

The most classical version of Vitali-Carathéodory theorem only ensures a large inequality
`f x ≤ g x`

. For applications to the fundamental theorem of calculus, though, the strict inequality
`f x < g x`

is important. Therefore, we prove the stronger version with strict inequalities in this
file. There is a price to pay: we require that the measure is `σ`

-finite, which is not necessary for
the classical Vitali-Carathéodory theorem. Since this is satisfied in all applications, this is
not a real problem.

## Sketch of proof #

Decomposing `f`

as the difference of its positive and negative parts, it suffices to show that a
positive function can be bounded from above by a lower semicontinuous function, and from below
by an upper semicontinuous function, with integrals close to that of `f`

.

For the bound from above, write `f`

as a series `∑' n, cₙ * indicator (sₙ)`

of simple functions.
Then, approximate `sₙ`

by a larger open set `uₙ`

with measure very close to that of `sₙ`

(this is
possible by regularity of the measure), and set `g = ∑' n, cₙ * indicator (uₙ)`

. It is
lower semicontinuous as a series of lower semicontinuous functions, and its integral is arbitrarily
close to that of `f`

.

For the bound from below, use finitely many terms in the series, and approximate `sₙ`

from inside by
a closed set `Fₙ`

. Then `∑ n < N, cₙ * indicator (Fₙ)`

is bounded from above by `f`

, it is
upper semicontinuous as a finite sum of upper semicontinuous functions, and its integral is
arbitrarily close to that of `f`

.

The main pain point in the implementation is that one needs to jump between the spaces `ℝ`

, `ℝ≥0`

,
`ℝ≥0∞`

and `EReal`

(and be careful that addition is not well behaved on `EReal`

), and between
`lintegral`

and `integral`

.

We first show the bound from above for simple functions and the nonnegative integral (this is the main nontrivial mathematical point), then deduce it for general nonnegative functions, first for the nonnegative integral and then for the Bochner integral.

Then we follow the same steps for the lower bound.

Finally, we glue them together to obtain the main statement
`exists_lt_lower_semicontinuous_integral_lt`

.

## Related results #

Are you looking for a result on approximation by continuous functions (not just semicontinuous)?
See result `MeasureTheory.Lp.boundedContinuousFunction_dense`

, in the file
`Mathlib/MeasureTheory/Function/ContinuousMapDense.lean`

.

## References #

[Rudin, *Real and Complex Analysis* (Theorem 2.24)][rudin2006real]

### Lower semicontinuous upper bound for nonnegative functions #

Given a simple function `f`

with values in `ℝ≥0`

, there exists a lower semicontinuous
function `g ≥ f`

with integral arbitrarily close to that of `f`

. Formulation in terms of
`lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given a measurable function `f`

with values in `ℝ≥0`

, there exists a lower semicontinuous
function `g ≥ f`

with integral arbitrarily close to that of `f`

. Formulation in terms of
`lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given a measurable function `f`

with values in `ℝ≥0`

in a sigma-finite space, there exists a
lower semicontinuous function `g > f`

with integral arbitrarily close to that of `f`

.
Formulation in terms of `lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given an almost everywhere measurable function `f`

with values in `ℝ≥0`

in a sigma-finite space,
there exists a lower semicontinuous function `g > f`

with integral arbitrarily close to that of `f`

.
Formulation in terms of `lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given an integrable function `f`

with values in `ℝ≥0`

in a sigma-finite space, there exists a
lower semicontinuous function `g > f`

with integral arbitrarily close to that of `f`

.
Formulation in terms of `integral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

### Upper semicontinuous lower bound for nonnegative functions #

Given a simple function `f`

with values in `ℝ≥0`

, there exists an upper semicontinuous
function `g ≤ f`

with integral arbitrarily close to that of `f`

. Formulation in terms of
`lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given an integrable function `f`

with values in `ℝ≥0`

, there exists an upper semicontinuous
function `g ≤ f`

with integral arbitrarily close to that of `f`

. Formulation in terms of
`lintegral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

Given an integrable function `f`

with values in `ℝ≥0`

, there exists an upper semicontinuous
function `g ≤ f`

with integral arbitrarily close to that of `f`

. Formulation in terms of
`integral`

.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`

.

### Vitali-Carathéodory theorem #

**Vitali-Carathéodory Theorem**: given an integrable real function `f`

, there exists an
integrable function `g > f`

which is lower semicontinuous, with integral arbitrarily close
to that of `f`

. This function has to be `EReal`

-valued in general.

**Vitali-Carathéodory Theorem**: given an integrable real function `f`

, there exists an
integrable function `g < f`

which is upper semicontinuous, with integral arbitrarily close to that
of `f`

. This function has to be `EReal`

-valued in general.