Abstract: |
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. |
BibTeX: |
@article{Hahn_Jordan_Decomposition-AFP,
author = {Marie Cousin and Mnacho Echenim and Hervé Guiol},
title = {The Hahn and Jordan Decomposition Theorems},
journal = {Archive of Formal Proofs},
month = nov,
year = 2021,
note = {\url{https://isa-afp.org/entries/Hahn_Jordan_Decomposition.html},
Formal proof development},
ISSN = {2150-914x},
}
|