Gluing measures along a cover #
A family of measures prescribed on the members of a family of measurable sets, agreeing on pairwise overlaps, comes from a single measure as soon as countably many of the sets cover the space, and that measure is unique. This is the descent step for measures that are only defined locally, such as the Riemannian volume, which is given chart by chart.
Main results #
TauCeti.existsUnique_restrict_eq: compatible measures on a family of measurable sets with a countable subcover glue to a unique measure.
theorem
TauCeti.existsUnique_restrict_eq
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{s : ι → Set α}
{μ : ι → MeasureTheory.Measure α}
(hs : ∀ (i : ι), MeasurableSet (s i))
{t : Set ι}
(ht : t.Countable)
(hcover : ⋃ i ∈ t, s i = Set.univ)
(h : ∀ (i j : ι), (μ i).restrict (s i ∩ s j) = (μ j).restrict (s i ∩ s j))
:
Measures μ i prescribed on measurable sets s i, agreeing on the pairwise overlaps, are the
restrictions of a unique measure, provided that countably many of the sets s i cover the space.
The overlap condition is necessary, and every s i is matched, not only those of the countable
subcover.