Unsigned Hahn decomposition theorem

This file proves the unsigned version of the Hahn decomposition theorem.

Main statements

• hahn_decomposition : Given two finite measures μ and ν, there exists a measurable set s such that any measurable set t included in s satisfies ν t ≤ μ t, and any measurable set u included in the complement of s satisfies μ u ≤ ν u.

Tags

Hahn decomposition

theorem MeasureTheory.hahn_decomposition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ∃ (s : Set α), MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ↑↑ν t ≤ ↑↑μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ↑↑μ t ≤ ↑↑ν t

Hahn decomposition theorem