mathlib documentation


Hahn decomposition #

This file proves the Hahn decomposition theorem (signed version). The Hahn decomposition theorem states that, given a signed measure s, there exist complementary, measurable sets i and j, such that i is positive and j is negative with respect to s; that is, s restricted on i is non-negative and s restricted on j is non-positive.

The Hahn decomposition theorem leads to many other results in measure theory, most notably, the Jordan decomposition theorem, the Lebesgue decomposition theorem and the Radon-Nikodym theorem.

Main results #

Notation #

We use the notations 0 ≤[i] s and s ≤[i] 0 to denote the usual definitions of a set i being positive/negative with respect to the signed measure s.

Tags #

Hahn decomposition theorem

exists_subset_restrict_nonpos #

In this section we will prove that a set i whose measure is negative contains a negative subset j with respect to the signed measure s (i.e. s ≤[j] 0), whose measure is negative. This lemma is used to prove the Hahn decomposition theorem.

To prove this lemma, we will construct a sequence of measurable sets $(A_n)_{n \in \mathbb{N}}$, such that, for all $n$, $s(A_{n + 1})$ is close to maximal among subsets of $i \setminus \bigcup_{k \le n} A_k$.

This sequence of sets does not necessarily exist. However, if this sequence terminates; that is, there does not exists any sets satisfying the property, the last $A_n$ will be a negative subset of negative measure, hence proving our claim.

In the case that the sequence does not terminate, it is easy to see that $i \setminus \bigcup_{k = 0}^\infty A_k$ is the required negative set.

To implement this in Lean, we define several auxilary definitions.

With these definitions, we are able consider the case where the sequence terminates separately, allowing us to prove exists_subset_restrict_nonpos.

A measurable set of negative measure has a negative subset of negative measure.

The set of measures of the set of measurable negative sets.


The Hahn decomposition thoerem: Given a signed measure s, there exist complement measurable sets i and j such that i is positive, j is negative.