# mathlibdocumentation

measure_theory.decomposition.signed_hahn

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

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

theorem measure_theory.signed_measure.exists_subset_restrict_nonpos {α : Type u_1} {i : set α} (hi : s i < 0) :
∃ (j : set α), j i s j < 0

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
theorem measure_theory.signed_measure.exists_compl_positive_negative {α : Type u_1}  :
∃ (i : set α),

Alternative formulation of measure_theory.signed_measure.exists_is_compl_positive_negative (the Hahn decomposition theorem) using set complements.

theorem measure_theory.signed_measure.exists_is_compl_positive_negative {α : Type u_1}  :
∃ (i j : set α), j

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.

theorem measure_theory.signed_measure.of_symm_diff_compl_positive_negative {α : Type u_1} {i j : set α} (hi : measurable_set i) (hj : measurable_set j) (hi' : ) (hj' : ) :
s (i j) = 0 s (i j) = 0

The symmetric difference of two Hahn decompositions has measure zero.