# mathlibdocumentation

measure_theory.measure.complex

# 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 measure_theory.measure.vector_measure and is known as measure_theory.complex_measure.

## Main definitions #

• measure_theory.complex_measure.re: obtains a signed measure s from a complex measure c such that s i = (c i).re for all measurable sets i.
• measure_theory.complex_measure.im: obtains a signed measure s from a complex measure c such that s i = (c i).im for all measurable sets i.
• measure_theory.signed_measure.to_complex_measure: given two signed measures s and t, s.to_complex_measure t provides a complex measure of the form s + it.
• measure_theory.complex_measure.equiv_signed_measure: is the equivalence between the complex measures and the type of the product of the signed measures with itself.

# Tags #

Complex measure

noncomputable def measure_theory.complex_measure.re {α : Type u_1} {m : measurable_space α} :

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

Equations
@[simp]
theorem measure_theory.complex_measure.re_apply {α : Type u_1} {m : measurable_space α}  :
noncomputable def measure_theory.complex_measure.im {α : Type u_1} {m : measurable_space α} :

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

Equations
@[simp]
theorem measure_theory.complex_measure.im_apply {α : Type u_1} {m : measurable_space α}  :

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

Equations
@[simp]
noncomputable def measure_theory.complex_measure.equiv_signed_measure {α : Type u_1} {m : measurable_space α} :

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

Equations
@[simp]
theorem measure_theory.complex_measure.equiv_signed_measure_symm_apply {α : Type u_1} {m : measurable_space α}  :
= measure_theory.complex_measure.equiv_signed_measure._match_1 _x
@[simp]
theorem measure_theory.complex_measure.equiv_signed_measureₗ_apply {α : Type u_1} {m : measurable_space α} {R : Type u_3} [semiring R] [ ]  :
noncomputable def measure_theory.complex_measure.equiv_signed_measureₗ {α : Type u_1} {m : measurable_space α} {R : Type u_3} [semiring R] [ ]  :

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

Equations
@[simp]
theorem measure_theory.complex_measure.equiv_signed_measureₗ_symm_apply {α : Type u_1} {m : measurable_space α} {R : Type u_3} [semiring R] [ ]  :