Email Gateway (Nov 26 2021 at 18:21): Email Gateway (Nov 26 2021 at 18:21):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
another new entry has been added to the AFP today:
The Hahn and Jordan Decomposition Theorems
by Marie Cousin, Mnacho Echenim and Hervé Guiol
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.
https://www.isa-afp.org/entries/Hahn_Jordan_Decomposition.html
Enjoy,
René
Last updated: Jul 15 2022 at 23:21 UTC