Vitali-Carathéodory theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Are you looking for a result on approximation by continuous functions (not just semicontinuous)? See result measure_theory.Lp.continuous_map_dense, in the file measure_theory.continuous_map_dense.

References #

Rudin, Real and Complex Analysis (Theorem 2.24)

Lower semicontinuous upper bound for nonnegative functions #

source

theorem measure_theory.simple_func.exists_le_lower_semicontinuous_lintegral_ge {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] (μ : measure_theory.measure α) [μ.weakly_regular] (f : measure_theory.simple_func α nnreal) {ε : ennreal} (ε0 : ε ≠ 0) :

∃ (g : α → nnreal), (∀ (x : α), ⇑f x ≤ g x) ∧ lower_semicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(⇑f x) ∂μ + ε

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.

source

theorem measure_theory.exists_le_lower_semicontinuous_lintegral_ge {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] (μ : measure_theory.measure α) [μ.weakly_regular] (f : α → ennreal) (hf : measurable f) {ε : ennreal} (εpos : ε ≠ 0) :

∃ (g : α → ennreal), (∀ (x : α), f x ≤ g x) ∧ lower_semicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε

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.

source

theorem measure_theory.exists_lt_lower_semicontinuous_lintegral_ge {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] (μ : measure_theory.measure α) [μ.weakly_regular] [measure_theory.sigma_finite μ] (f : α → nnreal) (fmeas : measurable f) {ε : ennreal} (ε0 : ε ≠ 0) :

∃ (g : α → ennreal), (∀ (x : α), ↑(f x) < g x) ∧ lower_semicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

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.

source

theorem measure_theory.exists_lt_lower_semicontinuous_lintegral_ge_of_ae_measurable {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] (μ : measure_theory.measure α) [μ.weakly_regular] [measure_theory.sigma_finite μ] (f : α → nnreal) (fmeas : ae_measurable f μ) {ε : ennreal} (ε0 : ε ≠ 0) :

∃ (g : α → ennreal), (∀ (x : α), ↑(f x) < g x) ∧ lower_semicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

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.

source

theorem measure_theory.exists_lt_lower_semicontinuous_integral_gt_nnreal {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {μ : measure_theory.measure α} [μ.weakly_regular] [measure_theory.sigma_finite μ] (f : α → nnreal) (fint : measure_theory.integrable (λ (x : α), ↑(f x)) μ) {ε : ℝ} (εpos : 0 < ε) :

∃ (g : α → ennreal), (∀ (x : α), ↑(f x) < g x) ∧ lower_semicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ measure_theory.integrable (λ (x : α), (g x).to_real) μ ∧ ∫ (x : α), (g x).to_real ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε

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 #

source

theorem measure_theory.simple_func.exists_upper_semicontinuous_le_lintegral_le {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {μ : measure_theory.measure α} [μ.weakly_regular] (f : measure_theory.simple_func α nnreal) (int_f : ∫⁻ (x : α), ↑(⇑f x) ∂μ ≠ ⊤) {ε : ennreal} (ε0 : ε ≠ 0) :

∃ (g : α → nnreal), (∀ (x : α), g x ≤ ⇑f x) ∧ upper_semicontinuous g ∧ ∫⁻ (x : α), ↑(⇑f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

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.

source

theorem measure_theory.exists_upper_semicontinuous_le_lintegral_le {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {μ : measure_theory.measure α} [μ.weakly_regular] (f : α → nnreal) (int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤) {ε : ennreal} (ε0 : ε ≠ 0) :

∃ (g : α → nnreal), (∀ (x : α), g x ≤ f x) ∧ upper_semicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

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.

source

theorem measure_theory.exists_upper_semicontinuous_le_integral_le {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {μ : measure_theory.measure α} [μ.weakly_regular] (f : α → nnreal) (fint : measure_theory.integrable (λ (x : α), ↑(f x)) μ) {ε : ℝ} (εpos : 0 < ε) :

∃ (g : α → nnreal), (∀ (x : α), g x ≤ f x) ∧ upper_semicontinuous g ∧ measure_theory.integrable (λ (x : α), ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ε ≤ ∫ (x : α), ↑(g x) ∂μ

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.