Hahn decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• measure_theory.signed_measure.exists_is_compl_positive_negative : the Hahn decomposition theorem.
• measure_theory.signed_measure.exists_subset_restrict_nonpos : A measurable set of negative measure contains a negative subset.

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.

• given the sets i and the natural number n, exists_one_div_lt s i n is the property that there exists a measurable set k ⊆ i such that 1 / (n + 1) < s k.
• given the sets i and that i is not negative, find_exists_one_div_lt s i is the least natural number n such that exists_one_div_lt s i n.
• given the sets i and that i is not negative, some_exists_one_div_lt chooses the set k from exists_one_div_lt s i (find_exists_one_div_lt s i).
• lastly, given the set i, restrict_nonpos_seq s i is the sequence of sets defined inductively where restrict_nonpos_seq s i 0 = some_exists_one_div_lt s (i \ ∅) and restrict_nonpos_seq s i (n + 1) = some_exists_one_div_lt s (i \ ⋃ k ≤ n, restrict_nonpos_seq k). This definition represents the sequence $(A_n)$ in the proof as described above.

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