Allocating disjoint sets of prescribed mass in a laminar family

Let μ be an atomless measure on a standard Borel space. The main result is a Hall-type theorem for a graded laminar family of sets of finite measure. Each member A i has a level lvl i. Distinct members of one level are disjoint, and a member of a deeper level lies inside or is disjoint from each member of a shallower level. If every member A i has room for its own demand m i together with the demands of all members strictly below it, then there are pairwise disjoint measurable sets Z i ⊆ A i with μ (Z i) = m i. This holds although the family may be infinitely deep.

The proof follows Pratelli. For each n the demands of levels below n are allocated. To pass to n + 1, the members of level n take any sets of the right mass; then, from level n - 1 up to level 0, each member gives up what the members below it now occupy and takes the same mass from free room in its own set, chosen by Sierpiński's theorem MeasureTheory.Measure.exists_subset_measure_eq_of_nullSingleton. A member loses at most the mass newly demanded below it, so each allocated set changes by summable amounts, and the Borel--Cantelli lemma lets the allocations converge.

This is the allocation step in Pratelli's proof that Monge's infimum equals Kantorovich's minimum for continuous costs and atomless sources: the members are the source sides of disjoint rectangles on which the cost nearly is constant, and each demand is the mass a transport plan puts on its rectangle.

Main statements

• MeasureTheory.Measure.exists_disjoint_subset_measure_eq_of_laminar: the laminar allocation theorem.

References

• A. Pratelli, On the equality between Monge's infimum and Kantorovich's minimum in optimal mass transportation, Ann. I. H. Poincaré Probab. Statist. 43 (2007), 1--13, §4, Steps II and III of the proof of Theorem B.

theorem MeasureTheory.Measure.exists_disjoint_subset_measure_eq_of_laminar {X : Type u_1} [MeasurableSpace X] [StandardBorelSpace X] (μ : Measure X) [NullSingletonClass μ] {ι : Type u_2} [Countable ι] {A : ι → Set X} (hA : ∀ (i : ι), MeasurableSet (A i)) (hAfin : ∀ (i : ι), μ (A i) ≠ ⊤) (lvl : ι → ℕ) (hlvl : ∀ (i j : ι), i ≠ j → lvl i = lvl j → Disjoint (A i) (A j)) (hlam : ∀ (i j : ι), lvl i < lvl j → A j ⊆ A i ∨ Disjoint (A i) (A j)) (m : ι → ENNReal) (hm : ∀ (i : ι), m i + ∑' (j : ↑{j : ι | lvl i < lvl j ∧ A j ⊆ A i}), m ↑j ≤ μ (A i)) : ∃ (Z : ι → Set X), (∀ (i : ι), MeasurableSet (Z i)) ∧ (∀ (i : ι), Z i ⊆ A i) ∧ Pairwise (Function.onFun Disjoint Z) ∧ ∀ (i : ι), μ (Z i) = m i

Allocation in a graded laminar family. Let μ be an atomless measure on a standard Borel space, and let A i be measurable sets of finite measure carrying levels lvl i, such that distinct members of one level are disjoint and a member of a deeper level lies inside or is disjoint from each member of a shallower level. If each A i has room for the demand m i together with the demands of all members strictly below it, then there are pairwise disjoint measurable sets Z i ⊆ A i with μ (Z i) = m i.

The family may be infinitely deep. This is the allocation of source sets in Pratelli's proof that Monge's infimum equals Kantorovich's minimum for continuous costs.