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 : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ℂ) : MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re

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

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

Equations

• MeasureTheory.ComplexMeasure.re = MeasureTheory.VectorMeasure.mapRangeₗ (↑Complex.reCLM) Complex.continuous_re

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

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

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

Equations

• MeasureTheory.ComplexMeasure.im = MeasureTheory.VectorMeasure.mapRangeₗ (↑Complex.imCLM) Complex.continuous_im

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

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

Equations

• s.toComplexMeasure t = { measureOf' := fun (i : Set α) => { re := ↑s i, im := ↑t i }, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

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

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

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

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.

@[simp]

theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply {α : Type u_1} {m : MeasurableSpace α} {R : Type u_3} [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_3} [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_3} [Semiring R] [Module R ℝ] [ContinuousConstSMul R ℝ] [ContinuousConstSMul R ℂ] : MeasureTheory.ComplexMeasure α ≃ₗ[R] MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α

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.

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