Unsigned Hahn decomposition theorem

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

Main definitions

• MeasureTheory.IsHahnDecomposition: characterizes a set where μ ≤ ν (and the reverse inequality on the complement),

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.
• exists_isHahnDecomposition : reformulation of hahn_decomposition using the IsHahnDecomposition structure which relies on the measure restriction.

Tags

Hahn decomposition

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

Hahn decomposition theorem

structure MeasureTheory.IsHahnDecomposition {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) (s : Set α) : Prop

A set where μ ≤ ν (and the reverse inequality on the complement), defined via measurable set and measure restriction comparisons.

• measurableSet : MeasurableSet s
• le_on : μ.restrict s ≤ ν.restrict s
• ge_on_compl : ν.restrict sᶜ ≤ μ.restrict sᶜ

theorem MeasureTheory.IsHahnDecomposition.compl {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} (h : IsHahnDecomposition μ ν s) : IsHahnDecomposition ν μ sᶜ

theorem MeasureTheory.exists_isHahnDecomposition {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : ∃ (s : Set α), IsHahnDecomposition μ ν s