The Hahn and Jordan Decomposition Theorems

Marie Cousin 📧, Mnacho Echenim 📧 and Hervé Guiol 📧

November 19, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In this work we formalize the Hahn decomposition theorem for signed measures, namely that any measure space for a signed measure can be decomposed into a positive and a negative set, where every measurable subset of the positive one has a positive measure, and every measurable subset of the negative one has a negative measure. We also formalize the Jordan decomposition theorem as a corollary, which states that the signed measure under consideration admits a unique decomposition into a difference of two positive measures, at least one of which is finite.


BSD License


Session Hahn_Jordan_Decomposition