MeasureTheory.hahn_decomposition

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

The **Hahn decomposition theorem** states that, for any type `α` that has a measurable space structure and given any two finite measures `μ` and `ν` on that space, there exists a set `s` which itself is measurable such that for every measurable subset `t` of `s`, the measure `ν` of `t` is less than or equal to the measure `μ` of `t`, and for every measurable subset `t` of the complement of `s`, the measure `μ` of `t` is less than or equal to the measure `ν` of `t`.

More concisely: For any measurable spaces `(α, Σ)` and measurable finiteness conditions on measures `μ` and `ν`, there exists a measurable set `s` such that for all measurable `t`, `μ(t) ≤ ν(t)` if `t ∋ s` and `ν(t) ≤ μ(t)` if `t ∉ s`.