# 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 measure s from a complex measure c such that s i = (c i).re for all measurable sets i.
• MeasureTheory.ComplexMeasure.im: obtains a signed measure s from a complex measure c such that s i = (c i).im for all measurable sets i.
• MeasureTheory.SignedMeasure.toComplexMeasure: given two signed measures s and t, s.to_complex_measure t provides a complex measure of the form s + 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

@[simp]
theorem MeasureTheory.ComplexMeasure.re_apply {α : Type u_1} {m : } (v : ) :
MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re
def MeasureTheory.ComplexMeasure.re {α : Type u_1} {m : } :

The real part of a complex measure is a signed measure.

Equations
• MeasureTheory.ComplexMeasure.re =
Instances For
@[simp]
theorem MeasureTheory.ComplexMeasure.im_apply {α : Type u_1} {m : } (v : ) :
MeasureTheory.ComplexMeasure.im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im
def MeasureTheory.ComplexMeasure.im {α : Type u_1} {m : } :

The imaginary part of a complex measure is a signed measure.

Equations
• MeasureTheory.ComplexMeasure.im =
Instances For
@[simp]
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_re {α : Type u_1} {m : } (s : ) (t : ) (i : Set α) :
((s.toComplexMeasure t) i).re = s i
@[simp]
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_im {α : Type u_1} {m : } (s : ) (t : ) (i : Set α) :
((s.toComplexMeasure t) i).im = t i
def MeasureTheory.SignedMeasure.toComplexMeasure {α : Type u_1} {m : } (s : ) (t : ) :

Given s and t signed measures, s + it is a complex measure

Equations
• s.toComplexMeasure t = { measureOf' := fun (i : Set α) => { re := s i, im := t i }, empty' := , not_measurable' := , m_iUnion' := }
Instances For
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply {α : Type u_1} {m : } {s : } {t : } {i : Set α} :
(s.toComplexMeasure t) i = { re := s i, im := t i }
theorem MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure {α : Type u_1} {m : } (c : ) :
(MeasureTheory.ComplexMeasure.re c).toComplexMeasure (MeasureTheory.ComplexMeasure.im c) = c
theorem MeasureTheory.SignedMeasure.re_toComplexMeasure {α : Type u_1} {m : } (s : ) (t : ) :
MeasureTheory.ComplexMeasure.re (s.toComplexMeasure t) = s
theorem MeasureTheory.SignedMeasure.im_toComplexMeasure {α : Type u_1} {m : } (s : ) (t : ) :
MeasureTheory.ComplexMeasure.im (s.toComplexMeasure t) = t
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply {α : Type u_1} {m : } :
∀ (x : ), MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x = match x with | (s, t) => s.toComplexMeasure t
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_apply {α : Type u_1} {m : } (c : ) :
MeasureTheory.ComplexMeasure.equivSignedMeasure c = (MeasureTheory.ComplexMeasure.re c, MeasureTheory.ComplexMeasure.im c)

The complex measures form an equivalence to the type of pairs of signed measures.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply {α : Type u_1} {m : } {R : Type u_3} [] [] [] [] :
∀ (a : ), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = MeasureTheory.ComplexMeasure.equivSignedMeasure.toFun a
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply {α : Type u_1} {m : } {R : Type u_3} [] [] [] [] :
∀ (a : ), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ.symm a = MeasureTheory.ComplexMeasure.equivSignedMeasure.invFun a
def MeasureTheory.ComplexMeasure.equivSignedMeasureₗ {α : Type u_1} {m : } {R : Type u_3} [] [] [] [] :

The complex measures form a linear isomorphism to the type of pairs of signed measures.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff {α : Type u_1} {m : } (c : ) :
MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.re c) μ MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.im c) μ