Complex measure #
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 s
and t
are signed measures.
The complex measure is defined to be vector measure over ℂ
, this definition can be found
in Mathlib/MeasureTheory/Measure/VectorMeasure.lean
and is known as
MeasureTheory.ComplexMeasure
.
Main definitions #
MeasureTheory.ComplexMeasure.re
: obtains a signed measures
from a complex measurec
such thats i = (c i).re
for all measurable setsi
.MeasureTheory.ComplexMeasure.im
: obtains a signed measures
from a complex measurec
such thats i = (c i).im
for all measurable setsi
.MeasureTheory.SignedMeasure.toComplexMeasure
: given two signed measuress
andt
,s.to_complex_measure t
provides a complex measure of the forms + it
.MeasureTheory.ComplexMeasure.equivSignedMeasure
: is the equivalence between the complex measures and the type of the product of the signed measures with itself.
Tags #
Complex measure
The real part of a complex measure is a signed measure.
Instances For
The imaginary part of a complex measure is a signed measure.
Instances For
Given s
and t
signed measures, s + it
is a complex measure
Instances For
The complex measures form an equivalence to the type of pairs of signed measures.
Instances For
The complex measures form a linear isomorphism to the type of pairs of signed measures.