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

source

@[simp]

theorem MeasureTheory.ComplexMeasure.re_apply {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ℂ) :

↑MeasureTheory.ComplexMeasure.re v = MeasureTheory.VectorMeasure.mapRange v (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re

source

def MeasureTheory.ComplexMeasure.re {α : Type u_1} {m : MeasurableSpace α} :

MeasureTheory.ComplexMeasure α →ₗ[ℝ ] MeasureTheory.SignedMeasure α

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

Instances For

source

@[simp]

theorem MeasureTheory.ComplexMeasure.im_apply {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ℂ) :

↑MeasureTheory.ComplexMeasure.im v = MeasureTheory.VectorMeasure.mapRange v (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im

source

def MeasureTheory.ComplexMeasure.im {α : Type u_1} {m : MeasurableSpace α} :

MeasureTheory.ComplexMeasure α →ₗ[ℝ ] MeasureTheory.SignedMeasure α

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

Instances For

source

@[simp]

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

(↑(MeasureTheory.SignedMeasure.toComplexMeasure s t) i).re = ↑s i

source

@[simp]

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

(↑(MeasureTheory.SignedMeasure.toComplexMeasure s t) i).im = ↑t i

source

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

Instances For

source

theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {t : MeasureTheory.SignedMeasure α} {i : Set α} :

↑(MeasureTheory.SignedMeasure.toComplexMeasure s t) i = { re := ↑s i, im := ↑t i }

source

theorem MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) :

MeasureTheory.SignedMeasure.toComplexMeasure (↑MeasureTheory.ComplexMeasure.re c) (↑MeasureTheory.ComplexMeasure.im c) = c

source

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

↑MeasureTheory.ComplexMeasure.re (MeasureTheory.SignedMeasure.toComplexMeasure s t) = s

source

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

↑MeasureTheory.ComplexMeasure.im (MeasureTheory.SignedMeasure.toComplexMeasure s t) = t

source

@[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) => MeasureTheory.SignedMeasure.toComplexMeasure s t

source

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

source

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.

Instances For

source

@[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 = Equiv.toFun MeasureTheory.ComplexMeasure.equivSignedMeasure a

source

@[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 α), ↑(LinearEquiv.symm MeasureTheory.ComplexMeasure.equivSignedMeasureₗ) a = Equiv.invFun MeasureTheory.ComplexMeasure.equivSignedMeasure a

source

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.

Instances For

source

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