# Documentation

Mathlib.MeasureTheory.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 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 =
def MeasureTheory.ComplexMeasure.re {α : Type u_1} {m : } :

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

Instances For
@[simp]
theorem MeasureTheory.ComplexMeasure.im_apply {α : Type u_1} {m : } (v : ) :
MeasureTheory.ComplexMeasure.im v =
def MeasureTheory.ComplexMeasure.im {α : Type u_1} {m : } :

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

Instances For
@[simp]
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_re {α : Type u_1} {m : } (s : ) (t : ) (i : Set α) :
().re = s i
@[simp]
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_im {α : Type u_1} {m : } (s : ) (t : ) (i : Set α) :
().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

Instances For
theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply {α : Type u_1} {m : } {s : } {t : } {i : Set α} :
= { re := s i, im := t i }
theorem MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure {α : Type u_1} {m : } (c : ) :
MeasureTheory.SignedMeasure.toComplexMeasure (MeasureTheory.ComplexMeasure.re c) (MeasureTheory.ComplexMeasure.im c) = c
theorem MeasureTheory.SignedMeasure.re_toComplexMeasure {α : Type u_1} {m : } (s : ) (t : ) :
MeasureTheory.ComplexMeasure.re () = s
theorem MeasureTheory.SignedMeasure.im_toComplexMeasure {α : Type u_1} {m : } (s : ) (t : ) :
MeasureTheory.ComplexMeasure.im () = t
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply {α : Type u_1} {m : } :
∀ (x : ), MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x = match x with | (s, 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.

Instances For
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply {α : Type u_1} {m : } {R : Type u_3} [] [] [] [] :
∀ (a : ), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = Equiv.toFun MeasureTheory.ComplexMeasure.equivSignedMeasure a
@[simp]
theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply {α : Type u_1} {m : } {R : Type u_3} [] [] [] [] :
∀ (a : ), ↑(LinearEquiv.symm MeasureTheory.ComplexMeasure.equivSignedMeasureₗ) a = Equiv.invFun MeasureTheory.ComplexMeasure.equivSignedMeasure 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.

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) μ