mathlib documentation

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 α} :

measure_theory.complex_measure α →ₗ[ℝ ] measure_theory.signed_measure α

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

Equations

measure_theory.complex_measure.re = measure_theory.vector_measure.map_rangeₗ ↑complex.re_clm complex.continuous_re

@[simp]

theorem measure_theory.complex_measure.re_apply {α : Type u_1} {m : measurable_space α} (v : measure_theory.vector_measure α ℂ) :

⇑measure_theory.complex_measure.re v = v.map_range complex.re_lm.to_add_monoid_hom complex.continuous_re

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

measure_theory.complex_measure α →ₗ[ℝ ] measure_theory.signed_measure α

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

Equations

measure_theory.complex_measure.im = measure_theory.vector_measure.map_rangeₗ ↑complex.im_clm complex.continuous_im

@[simp]

theorem measure_theory.complex_measure.im_apply {α : Type u_1} {m : measurable_space α} (v : measure_theory.vector_measure α ℂ) :

⇑measure_theory.complex_measure.im v = v.map_range complex.im_lm.to_add_monoid_hom complex.continuous_im

noncomputable def measure_theory.signed_measure.to_complex_measure {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) :

measure_theory.complex_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 α} :

⇑(s.to_complex_measure t) i = {re := ⇑s i, im := ⇑t i}

theorem measure_theory.complex_measure.to_complex_measure_to_signed_measure {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) :

(⇑measure_theory.complex_measure.re c).to_complex_measure (⇑measure_theory.complex_measure.im c) = c

theorem measure_theory.signed_measure.re_to_complex_measure {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) :

⇑measure_theory.complex_measure.re (s.to_complex_measure t) = s

theorem measure_theory.signed_measure.im_to_complex_measure {α : Type u_1} {m : measurable_space α} (s t : measure_theory.signed_measure α) :

⇑measure_theory.complex_measure.im (s.to_complex_measure t) = t

@[simp]

theorem measure_theory.complex_measure.equiv_signed_measure_apply {α : Type u_1} {m : measurable_space α} (c : measure_theory.complex_measure α) :

⇑measure_theory.complex_measure.equiv_signed_measure c = (⇑measure_theory.complex_measure.re c, ⇑measure_theory.complex_measure.im c)

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

measure_theory.complex_measure α ≃ measure_theory.signed_measure α × measure_theory.signed_measure α

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 α) :

⇑measure_theory.complex_measure.equiv_signed_measureₗ ᾰ = measure_theory.complex_measure.equiv_signed_measure.to_fun ᾰ

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 ℂ] :

measure_theory.complex_measure α ≃ₗ[R] measure_theory.signed_measure α × measure_theory.signed_measure α

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

Equations

measure_theory.complex_measure.equiv_signed_measureₗ = {to_fun := measure_theory.complex_measure.equiv_signed_measure.to_fun, map_add' := _, map_smul' := _, inv_fun := measure_theory.complex_measure.equiv_signed_measure.inv_fun, left_inv := _, right_inv := _}

@[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 α) :

⇑(measure_theory.complex_measure.equiv_signed_measureₗ.symm) ᾰ = measure_theory.complex_measure.equiv_signed_measure.inv_fun ᾰ

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

measure_theory.vector_measure.absolutely_continuous c μ ↔ measure_theory.vector_measure.absolutely_continuous (⇑measure_theory.complex_measure.re c) μ ∧ measure_theory.vector_measure.absolutely_continuous (⇑measure_theory.complex_measure.im c) μ