[isabelle] New in the AFP: The Hahn and Jordan Decomposition Theorems



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é


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.