Clarification regarding measures

Stream: new members

[Peter Hansen]

Greetings everyone,

In my first course in measure theory, I was introduced to the following definition of a measure:

Let $(X, \mathcal{A})$ be a measurable space. A measure (on $(X, \mathcal{A})$) is a set function $\mu: \mathcal{A} \rightarrow \overline{{\mathbb{R}}}_{\geq 0}$ that satisfies the following conditions:

1. $\mu (\varnothing)=0$
2. $\mu \left(\bigcup_{i=0}^{\infty} A_i\right) = \sum_{i=0}^{\infty} \mu \left(A_i\right)$ for all sequences $\left( A_i\right)_{i \in \mathbb{N}} \subseteq \mathcal{A}$ of pairwise disjoint sets

However, in Mathlib, it is defined as follows:

/-- A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure. -/
structure Measure (α : Type*) [MeasurableSpace α] extends OuterMeasure α where
m_iUnion ⦃f : ℕ → Set α⦄ :
(∀ i, MeasurableSet (f i)) →
Pairwise (Disjoint on f) → measureOf (⋃ i, f i) = ∑' i, measureOf (f i)
trimmed : toOuterMeasure.trim = toOuterMeasure

The definition of the trimmed outer measure is:

/-- We can trivially extend a function defined on a subclass of objects (with codomain `ℝ≥0∞`)
to all objects by defining it to be `∞` on the objects not in the class. -/
def extend (s : α) : ℝ≥0∞ :=
⨅ h : P s, m s h

/-- Given an arbitrary function on a subset of sets, we can define the outer measure corresponding
to it (this is the unique maximal outer measure that is at most `m` on the domain of `m`). -/
def inducedOuterMeasure : OuterMeasure α :=
ofFunction (extend m) (extend_empty P0 m0)

/-- Given an outer measure `m` we can forget its value on non-measurable sets, and then consider
`m.trim`, the unique maximal outer measure less than that function. -/
def trim : OuterMeasure α :=
inducedOuterMeasure (fun s _ => m s) MeasurableSet.empty m.empty

I’m struggling to fully grasp what is meant by "the outer measure is the canonical extension of the restricted measure." Also, I'm unsure of the motivation behind this added condition. What changes occur to an outer measure after it's trimmed? In the introduction to the definition of the trimmed outer measure, it states that the constructed measure forgets all values on non-measurable sets. In what sense are these values forgotten? Are they set to infinity?

In the literature that I have encountered, in Carathéodory's construction, an outer measure is first built from a pre-measure. As far as I can tell, Mathlib does not explicitly define a pre-measure, which I understand as a countably additive set function $\mu : R \to [0, \infty]$ with $\mu(\varnothing)=0$, where $R$ is a ring of sets. Am I correct in understanding that the extend function essentially constructs a pre-measure from any countably additive set function $m : \mathcal{P}(X) \to [0, \infty]$ satisfying $m(\varnothing)=0$? This seems reasonable, since the extend function appears to preserve both countable additivity and the zero-measure of the empty set.

I know that was a lot of questions, but if anyone of you would be so kind to take the time to answer just one of them, I would very grateful.

[Sébastien Gouëzel]

First, why is a measure defined on all sets, and not just measurable sets? It's for practicality: otherwise, whenever you write μ s, you would also need to provide a proof of measurability of s, and this would be extremely painful (just in the same way that we allow 0 / 0, or square roots of negative numbers -- this is the important concept of junk values).

Once you know that you want to define μ s for all s, you better use a good value for the junk value if s is not measurable (choosing good junk values is important to make sure as many theorems as possible hold with the weakest possible assumptions, which will make the life of the users easier). There is one canonical value which is used in most of the literature: require that μ s is the infimum of μ t over all measurable sets t containing s (that's the concept of outer measures). That's exactly the condition we require in the trimmed condition in the definition of a measure, although it's not completely obvious from the way it's written.

TLDR: we make sure that measures are defined on all sets for practicality reasons, and we make sure that the value for non-measurable sets is as reasonable as it can get with the trimmed condition in the definition of measures.

[Peter Hansen]

Thank you for taking the time to reply.

I can see the utility of using 'junk values' for non-measurable sets, although initially, I would have thought that discussions about measures on such sets might be more appropriately addressed in the context of outer measures. However, I've come to realize that the choices made in Mathlib that I don't immediately understand usually make sense in the end if you stare at them long enough.

Regarding your explanation of what constitutes a good junk value, it then seems reasonable that the following would hold by reflexivity:

example {s : Set X}  : m.trim s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ),
extend (fun s (_ :  MeasurableSet s) => m s) (t n) := by rfl

Though this seems like a good choice of a junk value — measuring the smallest measurable sets that contain a non-measurable set — I have not heard of the concept of canonical 'junk values' before. Could you suggest any materials or resources that discuss the importance and utility of choosing good junk values for non-measurable sets?

[Kevin Buzzard]

I think it's more a common sense thing rather than anything you can read about. You need to assign junk values and so you may as well make them as useful as possible

[Sébastien Gouëzel]

junk values are more a concept in formalization than in regular mathematics, where you can in theory let the reader check that all sets one is talking about are measurable (although in practice noone will ever do it). So you won't really find mathematics textbooks discussing this. Nevertheless, books on measure theory that need to engage with non-measurable sets most often require the property that the measure of any set is the infimum of the measure of measurable sets that contain them (see for instance Federer, Geometric Measure Theory, Definition 2.1.5), so that's definitely the right choice for us in mathlib.

[Peter Hansen]

Kevin Buzzard said:

I think it's more a common sense thing rather than anything you can read about. You need to assign junk values and so you may as well make them as useful as possible

Well, there is a price to be paid — another condition that has to be fulfilled.

Sébastien Gouëzel said:

junk values are more a concept in formalization than in regular mathematics, where you can in theory let the reader check that all sets one is talking about are measurable (although in practice noone will ever do it). So you won't really find mathematics textbooks discussing this. Nevertheless, books on measure theory that need to engage with non-measurable sets most often require the property that the measure of any set is the infimum of the measure of measurable sets that contain them (see for instance Federer, Geometric Measure Theory, Definition 2.1.5), so that's definitely the right choice for us in mathlib.

I'm currently writing a report on the construction of the Hausdorff Measure and have come across that book a few times. It certainly doesn’t hold your hand! In it, the definition of a regular outer measure goes like this:

A measure $\phi$ over $X$ is called regular if and only if for each set $A \subset X$ there exists a $\phi$ measurable set $B$ such that $A \subset B$ and $\phi(A)=\phi(B)$.

This concept aligns well with the Mathlib notion of a trimmed outer measure, particularly in light of the following theorems:

theorem exists_measurable_superset (μ : Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s  := by sorry

It seems the trimmed outer measure could be considered the regular outer measure associated with an outer measure. The main difference is that Federer defines a regular outer measure in terms of Carathéodory-measurable sets and not an arbitrary measurable space as in Mathlib. But I suppose, we usually construct a proper measure from an outer measure where all sets in the $\sigma$-algebra are also Carathéodory measurable, so it does not make much of a difference in the end.

I also had another question in my original post that I hope to have answered. You have already been gracious enough to answer first question, so I don’t expect you to answer this one as well. However, if not you, then perhaps someone else might:

In the literature, Carathéodory's construction often begins with a pre-measure, defined as a countably additive set function $\mu : R \to [0, \infty]$ satisfying $\mu(\varnothing)=0$, where $R$ is a ring of sets. Am I correct in understanding that the extend function essentially constructs a pre-measure from any countably additive set function $m : \mathcal{P}(X) \to [0, \infty]$ satisfying $m(\varnothing)=0$? This seems reasonable, since the extend function appears to preserve both countable additivity and the zero-measure of the empty set.

[Richard Osborn]

I see extend as taking a premeasure $m : R \to [0,\infty]$ and extending it to a premeasure of type $\mathcal{P}(X)\to[0,\infty]$ where $R\subseteq \mathcal{P}(X)$ is closed under countable union (I do not believe $R$ needs to be closed under set differences). See docs#MeasureTheory.extend_iUnion.