Selecting one representative from a countable family of local functions #
A countable family of functions that agree almost everywhere on their pairwise overlaps is represented by a single function, and that representative inherits local integrability on the union of the pieces.
theorem
CKN.exists_ae_eq_of_countable_family
{d : ℕ}
{V : ℕ → Set (Vec d)}
(hV : ∀ (n : ℕ), MeasurableSet (V n))
{g : ℕ → Vec d → ℝ}
(hagree : ∀ (m n : ℕ), g m =ᵐ[MeasureTheory.volume.restrict (V m ∩ V n)] g n)
:
∃ (G : Vec d → ℝ), ∀ (n : ℕ), G =ᵐ[MeasureTheory.volume.restrict (V n)] g n
A countable family of functions that agree almost everywhere on their pairwise overlaps admits a single function that agrees with every member almost everywhere on that member's own piece.
theorem
CKN.locallyIntegrableOn_of_ae_eq_cover
{d : ℕ}
{U : Set (Vec d)}
{V : ℕ → Set (Vec d)}
(hV : ∀ (n : ℕ), IsOpen (V n))
(hcover : U ⊆ ⋃ (n : ℕ), V n)
{G : Vec d → ℝ}
{g : ℕ → Vec d → ℝ}
(hg : ∀ (n : ℕ), MeasureTheory.LocallyIntegrableOn (g n) (V n) MeasureTheory.volume)
(hGg : ∀ (n : ℕ), G =ᵐ[MeasureTheory.volume.restrict (V n)] g n)
:
Local integrability passes from the members of an open countable cover to any function that agrees with each member almost everywhere on its piece.