Disjoint subsets of sets of small measure

If μ (s n) → 0, a subsequence of the measurable sets s n can be shrunk to pairwise disjoint measurable sets while losing at most η from the lower integrals of given functions of finite lower integral: remove from each chosen set all later chosen sets, choosing the subsequence so that the later sets carry lower integral at most η * 2⁻¹ ^ l for all earlier functions. Such disjoint sets feed the gliding hump arguments behind the Dunford–Pettis weak compactness criterion in L¹.

Main statements

• MeasureTheory.exists_strictMono_pairwise_disjoint_lintegral_le: shrinking a subsequence of sets of measure tending to zero to pairwise disjoint sets.

References

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

theorem MeasureTheory.exists_strictMono_pairwise_disjoint_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), ∫⁻ (x : α), f n x ∂μ ≠ ⊤) {s : ℕ → Set α} (hsm : ∀ (n : ℕ), MeasurableSet (s n)) (hs : Filter.Tendsto (fun (n : ℕ) => μ (s n)) Filter.atTop (nhds 0)) {η : ENNReal} (hη : η ≠ 0) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (B : ℕ → Set α), (∀ (j : ℕ), MeasurableSet (B j)) ∧ Pairwise (Function.onFun Disjoint B) ∧ (∀ (j : ℕ), B j ⊆ s (σ j)) ∧ ∀ (j : ℕ), ∫⁻ (x : α) in s (σ j), f (σ j) x ∂μ ≤ ∫⁻ (x : α) in B j, f (σ j) x ∂μ + η

If μ (s n) → 0, a subsequence of the measurable sets s n can be shrunk to pairwise disjoint measurable sets B j ⊆ s (σ j) such that the lower integral of f (σ j) over B j falls short of its lower integral over s (σ j) by at most η, for given functions f n of finite lower integral.