The de la Vallée Poussin criterion

A function Φ : ℝ → ℝ is superlinear when Φ t / t → ∞ as t → ∞. De la Vallée Poussin's criterion relates integrability and uniform integrability to integral bounds on Φ(‖f‖) for such Φ. This file proves the two directions used to exclude concentration of mass in approximation arguments: the existence of Φ for a single integrable function, and uniform control on small sets from a uniform bound on ∫ Φ(‖fᵢ‖).

• If f is integrable, there is a convex, monotone, superlinear Φ with Φ 0 = 0 and Φ ∘ ‖f‖ integrable (MeasureTheory.Integrable.exists_convexOn_superlinear_integrable). Convexity makes such a bound compatible with Jensen's inequality.
• If ∫ Φ(‖fᵢ‖) ≤ C < ∞ for all i and Φ is superlinear, then for every ε > 0 there is T with ∫_s ‖fᵢ‖ ≤ T μ(s) + ε for all i and all sets s (TauCeti.exists_setLIntegral_enorm_le_mul_add). In particular a family of a.e. strongly measurable functions with such a bound is uniformly integrable in Mathlib's sense (TauCeti.unifIntegrable_of_lintegral_ofReal_le).

Implementation notes

The function Φ of the first statement is the sum of ramps ∑ₖ max (x - tₖ) 0, where the levels tₖ ≥ k are chosen so that ∫ (‖f‖ - tₖ)⁺ ≤ δₖ for a summable sequence δₖ. Each ramp is convex and monotone, and the sum is superlinear because ever more ramps are active.

References

• C. de la Vallée Poussin, Sur l'intégrale de Lebesgue, Trans. Amer. Math. Soc. 16 (1915), 435–501.
• V. I. Bogachev, Measure Theory, Vol. I, Springer, 2007, §4.5.

theorem MeasureTheory.Integrable.exists_convexOn_superlinear_integrable {α : Type u_1} {F : Type u_2} [MeasurableSpace α] [NormedAddCommGroup F] {μ : Measure α} {f : α → F} (hf : Integrable f μ) : ∃ (Φ : ℝ → ℝ), Φ 0 = 0 ∧ Monotone Φ ∧ ConvexOn ℝ Set.univ Φ ∧ Filter.Tendsto (fun (t : ℝ) => Φ t / t) Filter.atTop Filter.atTop ∧ Integrable (fun (a : α) => Φ ‖f a‖) μ

De la Vallée Poussin's lemma. Every integrable function f remains integrable after composing its norm with some convex, monotone function Φ with Φ 0 = 0 that grows superlinearly, Φ t / t → ∞.

theorem TauCeti.exists_setLIntegral_enorm_le_mul_add {α : Type u_1} {F : Type u_2} {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} {Φ : ℝ → ℝ} (hΦ : Filter.Tendsto (fun (t : ℝ) => Φ t / t) Filter.atTop Filter.atTop) {f : ι → α → F} {C : ENNReal} (hC : C ≠ ⊤) (hf : ∀ (i : ι), ∫⁻ (a : α), ENNReal.ofReal (Φ ‖f i a‖) ∂μ ≤ C) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (T : NNReal), ∀ (i : ι) (s : Set α), ∫⁻ (a : α) in s, ‖f i a‖ₑ ∂μ ≤ ↑T * μ s + ε

De la Vallée Poussin's criterion, quantitative form. If Φ is superlinear and the functions f i satisfy the uniform bound ∫ Φ(‖f i‖) ≤ C < ∞, then for every ε > 0 there is a finite T with ∫_s ‖f i‖ ≤ T μ(s) + ε for every index i and every set s.

theorem TauCeti.unifIntegrable_of_lintegral_ofReal_le {α : Type u_1} {F : Type u_2} {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} {Φ : ℝ → ℝ} (hΦ : Filter.Tendsto (fun (t : ℝ) => Φ t / t) Filter.atTop Filter.atTop) {f : ι → α → F} (hfm : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) {C : ENNReal} (hC : C ≠ ⊤) (hf : ∀ (i : ι), ∫⁻ (a : α), ENNReal.ofReal (Φ ‖f i a‖) ∂μ ≤ C) : MeasureTheory.UnifIntegrable f 1 μ

De la Vallée Poussin's criterion. A family of a.e. strongly measurable functions with ∫ Φ(‖f i‖) ≤ C < ∞ for a superlinear Φ is uniformly integrable.