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 measures
from a complex measurec
such thats i = (c i).re
for all measurable setsi
.measure_theory.complex_measure.im
: obtains a signed measures
from a complex measurec
such thats i = (c i).im
for all measurable setsi
.measure_theory.signed_measure.to_complex_measure
: given two signed measuress
andt
,s.to_complex_measure t
provides a complex measure of the forms + 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
The real part of a complex measure is a signed measure.
@[simp]
theorem
measure_theory.complex_measure.re_apply
{α : Type u_1}
{m : measurable_space α}
(v : measure_theory.vector_measure α ℂ) :
The imaginary part of a complex measure is a signed measure.
@[simp]
theorem
measure_theory.complex_measure.im_apply
{α : Type u_1}
{m : measurable_space α}
(v : measure_theory.vector_measure α ℂ) :
noncomputable
def
measure_theory.signed_measure.to_complex_measure
{α : Type u_1}
{m : measurable_space α}
(s t : measure_theory.signed_measure α) :
Given s
and t
signed measures, s + it
is a complex measure
Equations
- s.to_complex_measure t = {measure_of' := λ (i : set α), {re := ⇑s i, im := ⇑t i}, empty' := _, not_measurable' := _, m_Union' := _}
@[simp]
theorem
measure_theory.signed_measure.to_complex_measure_apply_re
{α : Type u_1}
{m : measurable_space α}
(s t : measure_theory.signed_measure α)
(i : set α) :
(⇑(s.to_complex_measure t) i).re = ⇑s i
@[simp]
theorem
measure_theory.signed_measure.to_complex_measure_apply_im
{α : Type u_1}
{m : measurable_space α}
(s t : measure_theory.signed_measure α)
(i : set α) :
(⇑(s.to_complex_measure t) i).im = ⇑t i
theorem
measure_theory.signed_measure.to_complex_measure_apply
{α : Type u_1}
{m : measurable_space α}
{s t : measure_theory.signed_measure α}
{i : set α} :
theorem
measure_theory.complex_measure.to_complex_measure_to_signed_measure
{α : Type u_1}
{m : measurable_space α}
(c : measure_theory.complex_measure α) :
theorem
measure_theory.signed_measure.re_to_complex_measure
{α : Type u_1}
{m : measurable_space α}
(s t : measure_theory.signed_measure α) :
theorem
measure_theory.signed_measure.im_to_complex_measure
{α : Type u_1}
{m : measurable_space α}
(s t : measure_theory.signed_measure α) :
@[simp]
theorem
measure_theory.complex_measure.equiv_signed_measure_apply
{α : Type u_1}
{m : measurable_space α}
(c : measure_theory.complex_measure α) :
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
- measure_theory.complex_measure.equiv_signed_measure = {to_fun := λ (c : measure_theory.complex_measure α), (⇑measure_theory.complex_measure.re c, ⇑measure_theory.complex_measure.im c), inv_fun := λ (_x : measure_theory.signed_measure α × measure_theory.signed_measure α), measure_theory.complex_measure.equiv_signed_measure._match_1 _x, left_inv := _, right_inv := _}
- measure_theory.complex_measure.equiv_signed_measure._match_1 (s, t) = s.to_complex_measure t
@[simp]
theorem
measure_theory.complex_measure.equiv_signed_measure_symm_apply
{α : Type u_1}
{m : measurable_space α}
(_x : measure_theory.signed_measure α × measure_theory.signed_measure α) :
⇑(measure_theory.complex_measure.equiv_signed_measure.symm) _x = 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]
[module R ℝ]
[has_continuous_const_smul R ℝ]
[has_continuous_const_smul R ℂ]
(ᾰ : measure_theory.complex_measure α) :
noncomputable
def
measure_theory.complex_measure.equiv_signed_measureₗ
{α : Type u_1}
{m : measurable_space α}
{R : Type u_3}
[semiring R]
[module R ℝ]
[has_continuous_const_smul R ℝ]
[has_continuous_const_smul R ℂ] :
The complex measures form an linear isomorphism to the type of pairs of signed measures.
@[simp]
theorem
measure_theory.complex_measure.equiv_signed_measureₗ_symm_apply
{α : Type u_1}
{m : measurable_space α}
{R : Type u_3}
[semiring R]
[module R ℝ]
[has_continuous_const_smul R ℝ]
[has_continuous_const_smul R ℂ]
(ᾰ : measure_theory.signed_measure α × measure_theory.signed_measure α) :
theorem
measure_theory.complex_measure.absolutely_continuous_ennreal_iff
{α : Type u_1}
{m : measurable_space α}
(c : measure_theory.complex_measure α)
(μ : measure_theory.vector_measure α ennreal) :