Complex measure #
This file defines a complex measure to be a vector measure with codomain ℂ
.
Then we prove 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.
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
@[simp]
theorem
MeasureTheory.ComplexMeasure.re_apply
{α : Type u_1}
{m : MeasurableSpace α}
(v : MeasureTheory.VectorMeasure α ℂ)
:
MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re
The real part of a complex measure is a signed measure.
Equations
- MeasureTheory.ComplexMeasure.re = MeasureTheory.VectorMeasure.mapRangeₗ (↑Complex.reCLM) Complex.continuous_re
Instances For
@[simp]
theorem
MeasureTheory.ComplexMeasure.im_apply
{α : Type u_1}
{m : MeasurableSpace α}
(v : MeasureTheory.VectorMeasure α ℂ)
:
MeasureTheory.ComplexMeasure.im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im
The imaginary part of a complex measure is a signed measure.
Equations
- MeasureTheory.ComplexMeasure.im = MeasureTheory.VectorMeasure.mapRangeₗ (↑Complex.imCLM) Complex.continuous_im
Instances For
@[simp]
theorem
MeasureTheory.SignedMeasure.toComplexMeasure_apply_re
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
(i : Set α)
:
(↑(s.toComplexMeasure t) i).re = ↑s i
@[simp]
theorem
MeasureTheory.SignedMeasure.toComplexMeasure_apply_im
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
(i : Set α)
:
(↑(s.toComplexMeasure t) i).im = ↑t i
def
MeasureTheory.SignedMeasure.toComplexMeasure
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
:
Given s
and t
signed measures, s + it
is a complex measure
Equations
Instances For
theorem
MeasureTheory.SignedMeasure.toComplexMeasure_apply
{α : Type u_1}
{m : MeasurableSpace α}
{s : MeasureTheory.SignedMeasure α}
{t : MeasureTheory.SignedMeasure α}
{i : Set α}
:
↑(s.toComplexMeasure t) i = { re := ↑s i, im := ↑t i }
theorem
MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure
{α : Type u_1}
{m : MeasurableSpace α}
(c : MeasureTheory.ComplexMeasure α)
:
(MeasureTheory.ComplexMeasure.re c).toComplexMeasure (MeasureTheory.ComplexMeasure.im c) = c
theorem
MeasureTheory.SignedMeasure.re_toComplexMeasure
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
:
MeasureTheory.ComplexMeasure.re (s.toComplexMeasure t) = s
theorem
MeasureTheory.SignedMeasure.im_toComplexMeasure
{α : Type u_1}
{m : MeasurableSpace α}
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
:
MeasureTheory.ComplexMeasure.im (s.toComplexMeasure t) = t
@[simp]
theorem
MeasureTheory.ComplexMeasure.equivSignedMeasure_apply
{α : Type u_1}
{m : MeasurableSpace α}
(c : MeasureTheory.ComplexMeasure α)
:
MeasureTheory.ComplexMeasure.equivSignedMeasure c = (MeasureTheory.ComplexMeasure.re c, MeasureTheory.ComplexMeasure.im c)
@[simp]
theorem
MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply
{α : Type u_1}
{m : MeasurableSpace α}
:
∀ (x : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α),
MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x = match x with
| (s, t) => s.toComplexMeasure t
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 : MeasurableSpace α}
{R : Type u_2}
[Semiring R]
[Module R ℝ]
[ContinuousConstSMul R ℝ]
[ContinuousConstSMul R ℂ]
:
∀ (a : MeasureTheory.ComplexMeasure α),
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = MeasureTheory.ComplexMeasure.equivSignedMeasure.toFun a
@[simp]
theorem
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply
{α : Type u_1}
{m : MeasurableSpace α}
{R : Type u_2}
[Semiring R]
[Module R ℝ]
[ContinuousConstSMul R ℝ]
[ContinuousConstSMul R ℂ]
:
∀ (a : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α),
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ.symm a = MeasureTheory.ComplexMeasure.equivSignedMeasure.invFun a
def
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ
{α : Type u_1}
{m : MeasurableSpace α}
{R : Type u_2}
[Semiring R]
[Module R ℝ]
[ContinuousConstSMul R ℝ]
[ContinuousConstSMul R ℂ]
:
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 : MeasurableSpace α}
(c : MeasureTheory.ComplexMeasure α)
(μ : MeasureTheory.VectorMeasure α ENNReal)
:
MeasureTheory.VectorMeasure.AbsolutelyContinuous c μ ↔ MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.re c) μ ∧ MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.im c) μ