Contents on the null-measurable sets of a measure

A finitely additive set function vanishing on the null sets of a measure μ cannot distinguish sets that agree μ-almost everywhere (MeasureTheory.addContent_congr_ae). Since every μ-null-measurable set agrees almost everywhere with a measurable set, a content m on the measurable sets which vanishes on μ-null sets therefore extends uniquely to a content on the μ-null-measurable sets, that is, on the measurable sets of the completion of μ, still vanishing on μ-null sets. Its value at a null-measurable set s is m (toMeasurable μ s) (MeasureTheory.AddContent.completion).

Conversely, a content on the null-measurable sets restricts to the measurable sets (MeasureTheory.AddContent.map along id), and the extension of this restriction recovers the content, if it vanishes on null sets and, by convention, on sets that are not null-measurable. So contents on the measurable sets and on the null-measurable sets that vanish on null sets are the same thing. This is the form in which finitely additive set functions on the Borel sets of a group and on the measurable sets of its completed Haar measure correspond, for instance to describe the positive functionals on L∞. The extension preserves nonnegativity and invariance under a group action preserving μ.

Main definitions

• MeasureTheory.AddContent.completion: the extension of a content on the measurable sets, vanishing on μ-null sets, to the μ-null-measurable sets.

Main results

• MeasureTheory.AddContent.completion_apply: the extension takes the value m t at a null-measurable set that agrees almost everywhere with a measurable set t.
• MeasureTheory.AddContent.completion_unique, MeasureTheory.AddContent.completion_eq: any content on the null-measurable sets extending m and vanishing on null sets agrees with the extension at every null-measurable set, and equals it if it also vanishes, by convention, on sets that are not null-measurable. MeasureTheory.AddContent.completion_map_id recovers such a content as the extension of its restriction to the measurable sets.
• MeasureTheory.AddContent.forall_completion_smul_eq_iff: the extension is invariant under a measure-preserving group action exactly when m is invariant on measurable sets.

noncomputable def MeasureTheory.AddContent.completion {α : Type u_1} {G : Type u_2} [MeasurableSpace α] (μ : Measure α) [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) (hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0) : AddContent G {s : Set α | NullMeasurableSet s μ}

The extension of a content m on the measurable sets, vanishing on μ-null sets, to the μ-null-measurable sets. Its value at a null-measurable set s is the value of m at the measurable set toMeasurable μ s, which agrees with s almost everywhere. Its value at a set that is not null-measurable is zero.

theorem MeasureTheory.AddContent.completion_apply_eq_ite {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (s : Set α) : (completion μ m hm) s = if NullMeasurableSet s μ then m (toMeasurable μ s) else 0

The value of the extension of m: m (toMeasurable μ s) at a null-measurable set s, and zero elsewhere.

theorem MeasureTheory.AddContent.completion_apply {α : Type u_1} {G : Type u_2} {s t : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (hs : NullMeasurableSet s μ) (ht : MeasurableSet t) (hst : s =ᵐ[μ] t) : (completion μ m hm) s = m t

The extension of m takes the value m t at a null-measurable set that agrees almost everywhere with a measurable set t.

theorem MeasureTheory.AddContent.completion_apply_of_nullMeasurableSet {α : Type u_1} {G : Type u_2} {s : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (hs : NullMeasurableSet s μ) : (completion μ m hm) s = m (toMeasurable μ s)

The extension of m takes the value m (toMeasurable μ s) at a null-measurable set s.

@[simp]

theorem MeasureTheory.AddContent.completion_apply_of_measurableSet {α : Type u_1} {G : Type u_2} {s : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (hs : MeasurableSet s) : (completion μ m hm) s = m s

The extension of m agrees with m on measurable sets.

@[simp]

theorem MeasureTheory.AddContent.completion_of_not_nullMeasurableSet {α : Type u_1} {G : Type u_2} {s : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (hs : ¬NullMeasurableSet s μ) : (completion μ m hm) s = 0

The extension of m is zero at a set that is not null-measurable, by convention.

@[simp]

theorem MeasureTheory.AddContent.completion_of_measure_eq_zero {α : Type u_1} {G : Type u_2} {s : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} (hs : μ s = 0) : (completion μ m hm) s = 0

The extension of m vanishes on μ-null sets.

theorem MeasureTheory.AddContent.completion_unique {α : Type u_1} {G : Type u_2} {s : Set α} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} {m' : AddContent G {s : Set α | NullMeasurableSet s μ}} (hm' : ∀ (s : Set α), μ s = 0 → m' s = 0) (h : ∀ (s : Set α), MeasurableSet s → m' s = m s) (hs : NullMeasurableSet s μ) : (completion μ m hm) s = m' s

Any content on the null-measurable sets that agrees with m on measurable sets and vanishes on null sets agrees with the extension of m at every null-measurable set. See completion_eq for equality of contents, under the convention that the content vanishes on sets that are not null-measurable.

theorem MeasureTheory.AddContent.completion_eq {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} {m' : AddContent G {s : Set α | NullMeasurableSet s μ}} (hm' : ∀ (s : Set α), μ s = 0 → m' s = 0) (h : ∀ (s : Set α), MeasurableSet s → m' s = m s) (h' : ∀ (s : Set α), ¬NullMeasurableSet s μ → m' s = 0) : completion μ m hm = m'

A content on the null-measurable sets that agrees with m on measurable sets and vanishes on null sets, and by convention on sets that are not null-measurable, is the extension of m.

theorem MeasureTheory.AddContent.completion_map_id {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m' : AddContent G {s : Set α | NullMeasurableSet s μ}) (hm' : ∀ (s : Set α), μ s = 0 → m' s = 0) (h' : ∀ (s : Set α), ¬NullMeasurableSet s μ → m' s = 0) : completion μ (m'.map id ⋯) ⋯ = m'

A content on the null-measurable sets vanishing on null sets, and by convention on sets that are not null-measurable, is the extension of its restriction to the measurable sets.

theorem MeasureTheory.AddContent.completion_nonneg {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} [Preorder G] (h₀ : ∀ (s : Set α), MeasurableSet s → 0 ≤ m s) (s : Set α) : 0 ≤ (completion μ m hm) s

The extension of a nonnegative content is nonnegative.

theorem MeasureTheory.AddContent.completion_smul {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} {Γ : Type u_3} [Group Γ] [MulAction Γ α] [MeasurableConstSMul Γ α] [SMulInvariantMeasure Γ α μ] (h : ∀ (g : Γ) (s : Set α), MeasurableSet s → m (g • s) = m s) (g : Γ) (s : Set α) : (completion μ m hm) (g • s) = (completion μ m hm) s

If m is invariant on measurable sets under a group action preserving μ, then its extension is invariant on all sets.

theorem MeasureTheory.AddContent.forall_completion_smul_eq_iff {α : Type u_1} {G : Type u_2} [MeasurableSpace α] {μ : Measure α} [AddCommMonoid G] (m : AddContent G {s : Set α | MeasurableSet s}) {hm : ∀ (s : Set α), MeasurableSet s → μ s = 0 → m s = 0} {Γ : Type u_3} [Group Γ] [MulAction Γ α] [MeasurableConstSMul Γ α] [SMulInvariantMeasure Γ α μ] : (∀ (g : Γ) (s : Set α), (completion μ m hm) (g • s) = (completion μ m hm) s) ↔ ∀ (g : Γ) (s : Set α), MeasurableSet s → m (g • s) = m s

The extension of m is invariant under a group action preserving μ exactly when m is invariant on measurable sets.