# 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 #

• MeasureTheory.SignedMeasure.exists_isCompl_positive_negative : the Hahn decomposition theorem.
• MeasureTheory.SignedMeasure.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 auxiliary definitions.

• given the sets i and the natural number n, ExistsOneDivLT 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, findExistsOneDivLT s i is the least natural number n such that ExistsOneDivLT s i n.
• given the sets i and that i is not negative, someExistsOneDivLT chooses the set k from ExistsOneDivLT s i (findExistsOneDivLT s i).
• lastly, given the set i, restrictNonposSeq s i is the sequence of sets defined inductively where restrictNonposSeq s i 0 = someExistsOneDivLT s (i \ ∅) and restrictNonposSeq s i (n + 1) = someExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq 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.

theorem MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos {α : Type u_1} [] {s : } {i : Set α} (hi : s i < 0) :
∃ (j : Set α), j i

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

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

Equations
• s.measureOfNegatives = s ''
Instances For
theorem MeasureTheory.SignedMeasure.zero_mem_measureOfNegatives {α : Type u_1} [] {s : } :
0 s.measureOfNegatives
theorem MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives {α : Type u_1} [] {s : } :
BddBelow s.measureOfNegatives
theorem MeasureTheory.SignedMeasure.exists_compl_positive_negative {α : Type u_1} [] (s : ) :
∃ (i : Set α),

Alternative formulation of MeasureTheory.SignedMeasure.exists_isCompl_positive_negative (the Hahn decomposition theorem) using set complements.

theorem MeasureTheory.SignedMeasure.exists_isCompl_positive_negative {α : Type u_1} [] (s : ) :
∃ (i : Set α) (j : Set α),

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

theorem MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative {α : Type u_1} [] {s : } {i : Set α} {j : Set α} (hi : ) (hj : ) :
s (symmDiff i j) = 0 s (symmDiff i j) = 0

The symmetric difference of two Hahn decompositions has measure zero.