The Hahn and Jordan Decomposition Theorems

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

November 19, 2021


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