### 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.

### License

BSD License

### Topics

- Mathematics/Measure and integration

### Session Hahn_Jordan_Decomposition

- Extended_Reals_Sums_Compl
- Hahn_Jordan_Prelims
- Hahn_Jordan_Decomposition

## Cite

×

Hahn_Jordan_Decomposition-AFP

    @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   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Hahn_Jordan_Decomposition.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 26, 2021 : Isabelle2021