The Dunford–Pettis weak compactness criterion in L¹

For a finite measure μ, a subset A of scalar L¹(μ) is relatively weakly compact exactly when it is norm bounded and uniformly integrable: for every ε > 0 there is δ > 0 such that ∫ x in s, ‖f x‖ ∂μ ≤ ε for all f ∈ A and all measurable s with μ s ≤ δ. Here relative weak compactness means compactness of the weak closure of A, and uniform integrability is Mathlib's MeasureTheory.UnifIntegrable at exponent 1 for the representatives of the classes in A; together with the norm bound it is MeasureTheory.UniformIntegrable. By MeasureTheory.uniformIntegrable_iff, the latter is also the uniform tail-integral condition.

If A is uniformly integrable, then for each ε > 0 a truncation level C exists such that each f ∈ A lies within ε of its truncation f · 1_{‖f‖ < C}. The truncations lie in the image of a ball of L²(μ) under the inclusion L² → L¹, which is weakly compact because L² is reflexive. Grothendieck's lemma (TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact) then makes A relatively weakly compact.

Conversely, a relatively weakly compact set is bounded. If it were not uniformly integrable, there would be fₙ ∈ A and measurable sets of measure tending to zero on which the integrals of ‖fₙ‖ stay above some ε > 0. By Šmulian's theorem a subsequence converges weakly to some f, so the integrals of fₙ - f over each fixed measurable set tend to zero. Shrinking the sets to disjoint ones and applying the gliding hump lemma MeasureTheory.tendsto_setIntegral_norm_of_pairwise_disjoint gives a contradiction.

Main statements

• MeasureTheory.Lp.isCompact_closure_toWeakSpace_of_uniformIntegrable: uniformly integrable bounded subsets of L¹(μ) are relatively weakly compact.
• MeasureTheory.Lp.uniformIntegrable_of_isCompact_closure_toWeakSpace: relatively weakly compact subsets of L¹(μ) are bounded and uniformly integrable.
• MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_uniformIntegrable and MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_unifIntegrable: the Dunford–Pettis theorem, with and without the bound bundled into uniform integrability.
• MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_forall_setIntegral_le: the same with the uniform absolute continuity of the integrals ∫ x in s, ‖f x‖ ∂μ spelled out.

References

• N. Dunford and B. J. Pettis, Linear operations on summable functions, Trans. Amer. Math. Soc. 47 (1940), 323–392.
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §5.2.

theorem MeasureTheory.Lp.isCompact_closure_toWeakSpace_of_uniformIntegrable {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {A : Set ↥(Lp 𝕜 1 μ)} (hA : UniformIntegrable (fun (f : ↑A) => ↑↑↑f) 1 μ) : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(Lp 𝕜 1 μ)) '' A))

Dunford–Pettis theorem, sufficiency: for a finite measure, a bounded uniformly integrable subset of scalar L¹ has weakly compact closure.

theorem MeasureTheory.Lp.uniformIntegrable_of_isCompact_closure_toWeakSpace {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {A : Set ↥(Lp 𝕜 1 μ)} (hA : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(Lp 𝕜 1 μ)) '' A))) : UniformIntegrable (fun (f : ↑A) => ↑↑↑f) 1 μ

Dunford–Pettis theorem, necessity: for a finite measure, a subset of scalar L¹ with weakly compact closure is bounded and uniformly integrable.

theorem MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_uniformIntegrable {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {A : Set ↥(Lp 𝕜 1 μ)} : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(Lp 𝕜 1 μ)) '' A)) ↔ UniformIntegrable (fun (f : ↑A) => ↑↑↑f) 1 μ

Dunford–Pettis theorem. For a finite measure, a subset of scalar L¹ has weakly compact closure exactly when it is uniformly integrable together with a uniform norm bound.

theorem MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_unifIntegrable {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {A : Set ↥(Lp 𝕜 1 μ)} : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(Lp 𝕜 1 μ)) '' A)) ↔ Bornology.IsBounded A ∧ UnifIntegrable (fun (f : ↑A) => ↑↑↑f) 1 μ

Dunford–Pettis theorem. For a finite measure, a subset of scalar L¹ has weakly compact closure exactly when it is norm bounded and uniformly integrable.

theorem MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_forall_setIntegral_le {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {A : Set ↥(Lp 𝕜 1 μ)} : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(Lp 𝕜 1 μ)) '' A)) ↔ Bornology.IsBounded A ∧ ∀ ε > 0, ∃ δ > 0, ∀ f ∈ A, ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → ∫ (x : α) in s, ‖↑↑f x‖ ∂μ ≤ ε

Dunford–Pettis theorem, classical form. For a finite measure, a subset A of scalar L¹ has weakly compact closure exactly when it is norm bounded and the integrals of ‖f‖ are uniformly absolutely continuous: for every ε > 0 there is δ > 0 such that ∫ x in s, ‖f x‖ ∂μ ≤ ε for all f ∈ A and all measurable s with μ s ≤ δ.