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} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : Exists fun (s : Set α) => And (MeasurableSet s) (And (∀ (t : Set α), MeasurableSet t → HasSubset.Subset t s → LE.le (DFunLike.coe ν t) (DFunLike.coe μ t)) (∀ (t : Set α), MeasurableSet t → HasSubset.Subset t (HasCompl.compl s) → LE.le (DFunLike.coe μ t) (DFunLike.coe ν t)))

Hahn decomposition theorem