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

.

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

## Instances For

Alternative formulation of `measure_theory.signed_measure.exists_is_compl_positive_negative`

(the Hahn decomposition theorem) using set complements.

**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.

The symmetric difference of two Hahn decompositions has measure zero.