Real-valued contents, contents on all subsets, and pushforward

This file complements Mathlib's MeasureTheory.AddContent with the material needed to treat a finitely additive probability on all subsets of a type, given as an AddContent ℝ≥0∞ (Set.univ : Set (Set α)) of total mass one, as an ordinary real-valued nonnegative finitely additive set function, and to move such set functions along maps and group actions. Finitely additive probabilities on all subsets of a type are the set-theoretic form of means on bounded functions, and on a group the invariant ones correspond to invariant means; unlike measures, they cannot be replaced by countably additive set functions on a σ-algebra.

• For a ring of sets C, every content satisfies inclusion–exclusion, a content with values in an additive group satisfies the difference formula m (t \ s) = m t - m s for s ⊆ t, and a nonnegative content with values in an ordered additive monoid is monotone and finitely subadditive. Mathlib proves the last facts only for canonically ordered values such as ℝ≥0∞, which excludes real-valued contents. A content vanishing on the null sets of an outer measure takes the same value at sets that agree almost everywhere (MeasureTheory.addContent_congr_ae).
• MeasureTheory.AddContent.toReal turns a content with finite values on C into a real-valued one, and MeasureTheory.AddContent.ofReal turns a nonnegative real-valued content into an ℝ≥0∞-valued one. They are inverse on C, hence inverse when C is the set of all subsets.
• MeasureTheory.isSetRing_univ: all subsets form a ring of sets, so a set function on all subsets that vanishes at ∅ and is additive on disjoint pairs is a content (MeasureTheory.IsSetRing.addContent_of_union). A content on all subsets with canonically ordered values is bounded by its total mass, so an ℝ≥0∞-valued one is finite when its total mass is. A content on all subsets takes complements to differences with the total mass, for values in an additive group, or for ℝ≥0∞ values at sets of finite content.
• MeasureTheory.addContent_eq_natCard_div_natCard: on a finite type with a transitive scalar action, for instance a finite group acting on itself by left multiplication, an invariant content of total mass one on all subsets is normalized counting, m s = |s| / |α|.
• MeasureTheory.AddContent.map pushes a content forward along a map, with identity and composition laws. Pushforward along an equivariant map preserves invariance under a group action, and invariance of a content on all subsets is invariance under pushforward by every group element.

References

• A. Garrido, An introduction to amenable groups, Definitions 1.12–1.13.

theorem MeasureTheory.isSetRing_univ {α : Type u_1} : IsSetRing Set.univ

All subsets of a type form a ring of sets.

theorem MeasureTheory.addContent_union_add_inter {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_4} [AddCommMonoid G] {m : AddContent G C} (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m (s ∪ t) + m (s ∩ t) = m s + m t

Inclusion–exclusion for two sets in a ring of sets.

theorem MeasureTheory.addContent_sdiff_of_subset {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_4} [AddCommGroup G] {m : AddContent G C} (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m (t \ s) = m t - m s

In a ring of sets, a content with values in an additive group takes the difference of two nested sets to the difference of their values.

theorem MeasureTheory.addContent_congr_ae {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_4} {F : Type u_5} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {ν : F} [AddCommMonoid G] {m : AddContent G C} (hC : IsSetRing C) (hm : ∀ u ∈ C, ν u = 0 → m u = 0) (hs : s ∈ C) (ht : t ∈ C) (hst : s =ᵐ[ν] t) : m s = m t

A content on a ring of sets which vanishes on the null sets of C takes the same value at two sets of C that agree almost everywhere.

theorem MeasureTheory.addContent_mono_of_nonneg {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_4} [AddCommMonoid G] [PartialOrder G] [IsOrderedAddMonoid G] {m : AddContent G C} (hC : IsSetRing C) (hm : ∀ u ∈ C, 0 ≤ m u) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m s ≤ m t

A nonnegative content on a ring of sets is monotone. Unlike MeasureTheory.addContent_mono, the values need not be canonically ordered, so this applies to real-valued contents.

theorem MeasureTheory.addContent_union_le_of_nonneg {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_4} [AddCommMonoid G] [PartialOrder G] [IsOrderedAddMonoid G] {m : AddContent G C} (hC : IsSetRing C) (hm : ∀ u ∈ C, 0 ≤ m u) (hs : s ∈ C) (ht : t ∈ C) : m (s ∪ t) ≤ m s + m t

A nonnegative content on a ring of sets is subadditive.

theorem MeasureTheory.addContent_biUnion_le_of_nonneg {α : Type u_1} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] [PartialOrder G] [IsOrderedAddMonoid G] {m : AddContent G C} {ι : Type u_5} (hC : IsSetRing C) (hm : ∀ u ∈ C, 0 ≤ m u) {f : ι → Set α} {S : Finset ι} (hf : ∀ i ∈ S, f i ∈ C) : m (⋃ i ∈ S, f i) ≤ ∑ i ∈ S, m (f i)

A nonnegative content on a ring of sets is finitely subadditive.

theorem MeasureTheory.addContent_le_univ {α : Type u_1} {G : Type u_4} [AddCommMonoid G] [PartialOrder G] [CanonicallyOrderedAdd G] (m : AddContent G Set.univ) (s : Set α) : m s ≤ m Set.univ

A content on all subsets with canonically ordered values is bounded by its total mass.

theorem MeasureTheory.addContent_compl {α : Type u_1} {G : Type u_4} [AddCommGroup G] (m : AddContent G Set.univ) (s : Set α) : m sᶜ = m Set.univ - m s

A content on all subsets with values in an additive group takes complements to differences with the total mass.

theorem MeasureTheory.addContent_ne_top_of_univ_ne_top {α : Type u_1} {m : AddContent ENNReal Set.univ} (hm : m Set.univ ≠ ⊤) (s : Set α) : m s ≠ ⊤

A content on all subsets with finite total mass takes only finite values.

theorem MeasureTheory.addContent_compl_of_ne_top {α : Type u_1} {s : Set α} {m : AddContent ENNReal Set.univ} (hs : m s ≠ ⊤) : m sᶜ = m Set.univ - m s

An ℝ≥0∞-valued content on all subsets takes the complement of a set of finite content to the difference with the total mass.

theorem MeasureTheory.addContent_eq_natCard_div_natCard {α : Type u_1} {m : AddContent ENNReal Set.univ} {Γ : Type u_4} [SMul Γ α] [MulAction.IsPretransitive Γ α] [Finite α] (h₁ : m Set.univ = 1) (hm : ∀ (c : Γ) (s : Set α), m (c • s) = m s) (s : Set α) : m s = ↑(Nat.card ↑s) / ↑(Nat.card α)

On a finite type with a transitive scalar action, the only invariant finitely additive probability on all subsets is normalized counting, m s = |s| / |α|. No group or action laws are needed. In particular this applies to the left regular action of a finite group on itself.

def MeasureTheory.AddContent.toReal {α : Type u_1} {C : Set (Set α)} (m : AddContent ENNReal C) (hm : ∀ u ∈ C, m u ≠ ⊤) : AddContent ℝ C

The real-valued content obtained from an ℝ≥0∞-valued content which is finite on C.

@[simp]

theorem MeasureTheory.AddContent.toReal_apply {α : Type u_1} {C : Set (Set α)} (m : AddContent ENNReal C) (hm : ∀ u ∈ C, m u ≠ ⊤) (u : Set α) : (m.toReal hm) u = (m u).toReal

def MeasureTheory.AddContent.ofReal {α : Type u_1} {C : Set (Set α)} (m : AddContent ℝ C) (hm : ∀ u ∈ C, 0 ≤ m u) : AddContent ENNReal C

The ℝ≥0∞-valued content obtained from a real-valued content which is nonnegative on C.

@[simp]

theorem MeasureTheory.AddContent.ofReal_apply {α : Type u_1} {C : Set (Set α)} (m : AddContent ℝ C) (hm : ∀ u ∈ C, 0 ≤ m u) (u : Set α) : (m.ofReal hm) u = ENNReal.ofReal (m u)

theorem MeasureTheory.AddContent.toReal_nonneg {α : Type u_1} {C : Set (Set α)} (m : AddContent ENNReal C) (hm : ∀ u ∈ C, m u ≠ ⊤) (u : Set α) : 0 ≤ (m.toReal hm) u

theorem MeasureTheory.AddContent.ofReal_ne_top {α : Type u_1} {C : Set (Set α)} (m : AddContent ℝ C) (hm : ∀ u ∈ C, 0 ≤ m u) (u : Set α) : (m.ofReal hm) u ≠ ⊤

theorem MeasureTheory.AddContent.ofReal_toReal_apply {α : Type u_1} {C : Set (Set α)} {s : Set α} (m : AddContent ENNReal C) (hm : ∀ u ∈ C, m u ≠ ⊤) (hs : s ∈ C) : ((m.toReal hm).ofReal ⋯) s = m s

theorem MeasureTheory.AddContent.toReal_ofReal_apply {α : Type u_1} {C : Set (Set α)} {s : Set α} (m : AddContent ℝ C) (hm : ∀ u ∈ C, 0 ≤ m u) (hs : s ∈ C) : ((m.ofReal hm).toReal ⋯) s = m s

@[simp]

theorem MeasureTheory.AddContent.ofReal_toReal {α : Type u_1} (m : AddContent ENNReal Set.univ) (hm : ∀ u ∈ Set.univ, m u ≠ ⊤) : (m.toReal hm).ofReal ⋯ = m

On all subsets, ofReal is a left inverse of toReal.

@[simp]

theorem MeasureTheory.AddContent.toReal_ofReal {α : Type u_1} (m : AddContent ℝ Set.univ) (hm : ∀ u ∈ Set.univ, 0 ≤ m u) : (m.ofReal hm).toReal ⋯ = m

On all subsets, toReal is a left inverse of ofReal.

def MeasureTheory.AddContent.map {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] {D : Set (Set β)} (m : AddContent G C) (f : α → β) (hf : ∀ u ∈ D, f ⁻¹' u ∈ C) : AddContent G D

The pushforward of a content along a map f, defined on a family D of sets whose preimages under f lie in C.

@[simp]

theorem MeasureTheory.AddContent.map_apply {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] {D : Set (Set β)} (m : AddContent G C) (f : α → β) (hf : ∀ u ∈ D, f ⁻¹' u ∈ C) (u : Set β) : (m.map f hf) u = m (f ⁻¹' u)

@[simp]

theorem MeasureTheory.AddContent.map_id {α : Type u_1} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] (m : AddContent G C) : m.map id ⋯ = m

theorem MeasureTheory.AddContent.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] {D : Set (Set β)} {E : Set (Set γ)} (m : AddContent G C) {f : α → β} {g : β → γ} (hf : ∀ u ∈ D, f ⁻¹' u ∈ C) (hg : ∀ u ∈ E, g ⁻¹' u ∈ D) : (m.map f hf).map g hg = m.map (g ∘ f) ⋯

theorem MeasureTheory.AddContent.map_apply_smul_set {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {G : Type u_4} [AddCommMonoid G] {D : Set (Set β)} {Γ : Type u_5} [Group Γ] [MulAction Γ α] [MulAction Γ β] {F : Type u_6} [FunLike F α β] [MulActionHomClass F Γ α β] (m : AddContent G C) (f : F) (hf : ∀ u ∈ D, ⇑f ⁻¹' u ∈ C) (hm : ∀ (c : Γ), ∀ u ∈ C, m (c • u) = m u) (c : Γ) {u : Set β} (hu : u ∈ D) : (m.map (⇑f) hf) (c • u) = (m.map (⇑f) hf) u

Pushforward along an equivariant map preserves invariance under a group action.

theorem MeasureTheory.AddContent.map_smul_apply {α : Type u_1} {G : Type u_4} [AddCommMonoid G] {Γ : Type u_5} [Group Γ] [MulAction Γ α] (m : AddContent G Set.univ) (c : Γ) (u : Set α) : (m.map (fun (x : α) => c • x) ⋯) u = m (c⁻¹ • u)

Pushing a content on all subsets forward along the action of c evaluates it on translates by c⁻¹.

theorem MeasureTheory.AddContent.forall_map_smul_eq_iff {α : Type u_1} {G : Type u_4} [AddCommMonoid G] {Γ : Type u_5} [Group Γ] [MulAction Γ α] (m : AddContent G Set.univ) : (∀ (c : Γ), m.map (fun (x : α) => c • x) ⋯ = m) ↔ ∀ (c : Γ) (u : Set α), m (c • u) = m u

A content on all subsets is invariant under a group action if and only if it is fixed by pushforward along the action of every group element.