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

@[reducible, inline]

abbrev MeasureTheory.ComplexMeasure (α : Type u_2) [MeasurableSpace α] : Type u_2

A ComplexMeasure is a ℂ-vector measure.

def MeasureTheory.ComplexMeasure.re {α : Type u_1} {m : MeasurableSpace α} : ComplexMeasure α →ₗ[ℝ] SignedMeasure α

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

@[simp]

theorem MeasureTheory.ComplexMeasure.re_apply {α : Type u_1} {m : MeasurableSpace α} (v : VectorMeasure α ℂ) : re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re

def MeasureTheory.ComplexMeasure.im {α : Type u_1} {m : MeasurableSpace α} : ComplexMeasure α →ₗ[ℝ] SignedMeasure α

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

@[simp]

theorem MeasureTheory.ComplexMeasure.im_apply {α : Type u_1} {m : MeasurableSpace α} (v : VectorMeasure α ℂ) : im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im

def MeasureTheory.SignedMeasure.toComplexMeasure {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) : ComplexMeasure α

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

@[simp]

theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_im {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (i : Set α) : (↑(s.toComplexMeasure t) i).im = ↑t i

@[simp]

theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_re {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) (i : Set α) : (↑(s.toComplexMeasure t) i).re = ↑s i

theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {s t : 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 : ComplexMeasure α) : (re c).toComplexMeasure (im c) = c

theorem MeasureTheory.SignedMeasure.re_toComplexMeasure {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) : ComplexMeasure.re (s.toComplexMeasure t) = s

theorem MeasureTheory.SignedMeasure.im_toComplexMeasure {α : Type u_1} {m : MeasurableSpace α} (s t : SignedMeasure α) : ComplexMeasure.im (s.toComplexMeasure t) = t

def MeasureTheory.ComplexMeasure.equivSignedMeasure {α : Type u_1} {m : MeasurableSpace α} : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α

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

@[simp]

theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (c : ComplexMeasure α) : equivSignedMeasure c = (re c, im c)

@[simp]

theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply {α : Type u_1} {m : MeasurableSpace α} (x✝ : SignedMeasure α × SignedMeasure α) : equivSignedMeasure.symm x✝ = match x✝ with | (s, t) => s.toComplexMeasure t

def MeasureTheory.ComplexMeasure.equivSignedMeasureₗ {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [Semiring R] [Module R ℝ] [ContinuousConstSMul R ℝ] [ContinuousConstSMul R ℂ] : ComplexMeasure α ≃ₗ[R] SignedMeasure α × SignedMeasure α

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

@[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✝ : SignedMeasure α × SignedMeasure α) : equivSignedMeasureₗ.symm a✝ = equivSignedMeasure.invFun a✝

@[simp]

theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [Semiring R] [Module R ℝ] [ContinuousConstSMul R ℝ] [ContinuousConstSMul R ℂ] (a✝ : ComplexMeasure α) : equivSignedMeasureₗ a✝ = equivSignedMeasure.toFun a✝

theorem MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff {α : Type u_1} {m : MeasurableSpace α} (c : ComplexMeasure α) (μ : VectorMeasure α ENNReal) : VectorMeasure.AbsolutelyContinuous c μ ↔ VectorMeasure.AbsolutelyContinuous (re c) μ ∧ VectorMeasure.AbsolutelyContinuous (im c) μ