Set integrals of a sequence along disjoint sets

Let h n be integrable functions such that ∫ x in s, h n x ∂μ → 0 for every measurable set s, as happens for a weakly null sequence in L¹. If the measurable sets B n are pairwise disjoint, then also ∫ x in B n, h n x ∂μ → 0, although the set of integration moves with n. For real or complex functions the conclusion improves to ∫ x in B n, ‖h n x‖ ∂μ → 0, by splitting B n into the sets where the real and imaginary parts of h n have a fixed sign.

The proof is a gliding hump argument. If the conclusion fails, choose indices n₀ < n₁ < ⋯ along which ‖∫ x in B nⱼ, h nⱼ x ∂μ‖ ≥ ε, the integral of h nⱼ over the union of the earlier sets B nᵢ is small, and the integral of ‖h nⱼ‖ over all later sets B m is small. Then the integrals of h nⱼ over the single set ⋃ j, B nⱼ stay away from zero.

Together with MeasureTheory.exists_strictMono_pairwise_disjoint_lintegral_le, which produces such disjoint sets from sets of small measure, these give the uniform integrability of weakly convergent sequences in L¹, which is the hard half of the Dunford–Pettis weak compactness criterion.

Main statements

• MeasureTheory.tendsto_setIntegral_iUnion_ge_of_pairwise_disjoint: integrals over the tails ⋃ m ≥ M, B m of a pairwise disjoint sequence tend to zero.
• MeasureTheory.tendsto_setIntegral_of_pairwise_disjoint: integrals along disjoint sets of a sequence whose integrals over each fixed measurable set tend to zero tend to zero.
• MeasureTheory.tendsto_setIntegral_norm_of_pairwise_disjoint: the same for the integrals of the norm, for real or complex functions.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §5.2, for the role of these statements in the Dunford–Pettis theorem.

theorem MeasureTheory.tendsto_setIntegral_iUnion_ge_of_pairwise_disjoint {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : α → E} (hg : Integrable g μ) {B : ℕ → Set α} (hBm : ∀ (n : ℕ), MeasurableSet (B n)) (hB : Pairwise (Function.onFun Disjoint B)) : Filter.Tendsto (fun (M : ℕ) => ∫ (x : α) in ⋃ (m : ℕ), ⋃ (_ : m ≥ M), B m, g x ∂μ) Filter.atTop (nhds 0)

The integrals of an integrable function over the tails ⋃ m ≥ M, B m of a pairwise disjoint sequence of measurable sets tend to zero.

theorem MeasureTheory.tendsto_setIntegral_of_pairwise_disjoint {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : ℕ → α → E} (hh : ∀ (n : ℕ), Integrable (h n) μ) (hlim : ∀ (s : Set α), MeasurableSet s → Filter.Tendsto (fun (n : ℕ) => ∫ (x : α) in s, h n x ∂μ) Filter.atTop (nhds 0)) {B : ℕ → Set α} (hBm : ∀ (n : ℕ), MeasurableSet (B n)) (hB : Pairwise (Function.onFun Disjoint B)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α) in B n, h n x ∂μ) Filter.atTop (nhds 0)

If the integrals of h n over every fixed measurable set tend to zero, then so do the integrals of h n over the n-th set of a pairwise disjoint sequence of measurable sets.

theorem MeasureTheory.tendsto_setIntegral_norm_of_pairwise_disjoint {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {h : ℕ → α → 𝕜} (hh : ∀ (n : ℕ), Integrable (h n) μ) (hlim : ∀ (s : Set α), MeasurableSet s → Filter.Tendsto (fun (n : ℕ) => ∫ (x : α) in s, h n x ∂μ) Filter.atTop (nhds 0)) {B : ℕ → Set α} (hBm : ∀ (n : ℕ), MeasurableSet (B n)) (hB : Pairwise (Function.onFun Disjoint B)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α) in B n, ‖h n x‖ ∂μ) Filter.atTop (nhds 0)

If the integrals of the real or complex functions h n over every fixed measurable set tend to zero, then the integrals of ‖h n‖ over the n-th set of a pairwise disjoint sequence of measurable sets tend to zero.