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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} (hi : ↑s i < 0) : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ ↑s j < 0

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

def MeasureTheory.SignedMeasure.measureOfNegatives {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : Set ℝ

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

Equations

• s.measureOfNegatives = ↑s '' {B : Set α | MeasurableSet B ∧ MeasureTheory.VectorMeasure.restrict s B ≤ MeasureTheory.VectorMeasure.restrict 0 B}

theorem MeasureTheory.SignedMeasure.zero_mem_measureOfNegatives {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} : 0 ∈ s.measureOfNegatives

theorem MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} : BddBelow s.measureOfNegatives

theorem MeasureTheory.SignedMeasure.exists_compl_positive_negative {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : ∃ (i : Set α), MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ

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} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : ∃ (i : Set α) (j : Set α), MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasurableSet j ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j

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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} {j : Set α} (hi : MeasurableSet i) (hj : MeasurableSet j) (hi' : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ) (hj' : MeasureTheory.VectorMeasure.restrict 0 j ≤ MeasureTheory.VectorMeasure.restrict s j ∧ MeasureTheory.VectorMeasure.restrict s jᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 jᶜ) : ↑s (symmDiff i j) = 0 ∧ ↑s (symmDiff iᶜ jᶜ) = 0

The symmetric difference of two Hahn decompositions has measure zero.