Complex measure #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves some elementary results about complex measures. In particular, we prove that
a complex measure is always in the form
s + it where
t are signed measures.
The complex measure is defined to be vector measure over
ℂ, this definition can be found
measure_theory.measure.vector_measure and is known as
Main definitions #
The real part of a complex measure is a signed measure.
The imaginary part of a complex measure is a signed measure.
t signed measures,
s + it is a complex measure
The complex measures form an equivalence to the type of pairs of signed measures.
The complex measures form an linear isomorphism to the type of pairs of signed measures.