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.