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