Integration against scalar measures

For an RCLike field 𝕜 and a 𝕜-valued vector measure μ of finite variation, the integral of a function f : X → 𝕜 is Mathlib's vector-measure integral through the multiplication pairing, ∫ᵛ x, f x ∂[mul ℝ 𝕜; μ]. Mathlib proves its real-linearity in f and in μ. This file supplies the remaining scalar calculus of this integral: homogeneity over 𝕜, and the reduction of a scalar measure to signed measures through its real and imaginary parts. These are the comparisons needed to treat complex measures by the Jordan decomposition of their real and imaginary parts, as in uniqueness theorems for measures on compact spaces.

The comparisons for the real and imaginary parts and the real-to-scalar embedding are instances of the naturality of the vector-measure integral, map_integral_comp_eq_integral_mapRangeL in TauCeti.MeasureTheory.VectorMeasure.Integral.

Main declarations

• MeasureTheory.VectorMeasure.integral_const_mul and MeasureTheory.VectorMeasure.integral_smul_vectorMeasure_mul: 𝕜-homogeneity of the scalar integral in the integrand and in the measure.
• MeasureTheory.VectorMeasure.scalarMeasureRealPart, MeasureTheory.VectorMeasure.scalarMeasureImagPart: the real and imaginary parts of a scalar measure, as real-linear maps to signed measures.
• MeasureTheory.VectorMeasure.scalarMeasureOfReal: a signed measure as a scalar measure.
• MeasureTheory.VectorMeasure.scalarMeasureOfReal_realPart_add_I_smul_imagPart: the reconstruction μ = re μ + I • im μ.
• MeasureTheory.VectorMeasure.isFiniteMeasure_variation: every scalar measure has finite variation.
• MeasureTheory.VectorMeasure.re_integral_ofReal, MeasureTheory.VectorMeasure.im_integral_ofReal: the real and imaginary parts of the integral of a real function are its integrals against the real and imaginary parts of the measure.
• MeasureTheory.VectorMeasure.integral_mul_eq_integral_posPart_sub_integral_negPart: the integral against a signed measure through its Jordan decomposition.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw–Hill, 1987, Chapter 6.

theorem MeasureTheory.VectorMeasure.integral_const_mul {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (c : 𝕜) (f : X → 𝕜) : ∫ᵛ (x : X), c * f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = c * ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ]

The integral against a scalar measure is 𝕜-homogeneous in the integrand.

@[simp]

theorem MeasureTheory.VectorMeasure.integral_smul_vectorMeasure_mul {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (c : 𝕜) (f : X → 𝕜) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; c • μ] = c * ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ]

The integral against a scalar measure is 𝕜-homogeneous in the measure.

noncomputable def MeasureTheory.VectorMeasure.scalarMeasureRealPart {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] : VectorMeasure X 𝕜 →ₗ[ℝ] SignedMeasure X

The real part of a scalar measure, as a signed measure. For 𝕜 = ℂ this is MeasureTheory.ComplexMeasure.re (scalarMeasureRealPart_eq_re).

noncomputable def MeasureTheory.VectorMeasure.scalarMeasureImagPart {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] : VectorMeasure X 𝕜 →ₗ[ℝ] SignedMeasure X

The imaginary part of a scalar measure, as a signed measure. For 𝕜 = ℂ this is MeasureTheory.ComplexMeasure.im (scalarMeasureImagPart_eq_im).

noncomputable def MeasureTheory.VectorMeasure.scalarMeasureOfReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] : SignedMeasure X →ₗ[ℝ] VectorMeasure X 𝕜

A signed measure regarded as a scalar measure, through the embedding ℝ → 𝕜.

@[simp]

theorem MeasureTheory.VectorMeasure.scalarMeasureRealPart_apply {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (s : Set X) : (scalarMeasureRealPart μ) s = RCLike.re (μ s)

@[simp]

theorem MeasureTheory.VectorMeasure.scalarMeasureImagPart_apply {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (s : Set X) : (scalarMeasureImagPart μ) s = RCLike.im (μ s)

@[simp]

theorem MeasureTheory.VectorMeasure.scalarMeasureOfReal_apply {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (σ : SignedMeasure X) (s : Set X) : (scalarMeasureOfReal σ) s = ↑(σ s)

@[simp]

theorem MeasureTheory.VectorMeasure.scalarMeasureRealPart_scalarMeasureOfReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (σ : SignedMeasure X) : scalarMeasureRealPart (scalarMeasureOfReal σ) = σ

@[simp]

theorem MeasureTheory.VectorMeasure.scalarMeasureImagPart_scalarMeasureOfReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (σ : SignedMeasure X) : scalarMeasureImagPart (scalarMeasureOfReal σ) = 0

theorem MeasureTheory.VectorMeasure.scalarMeasureOfReal_realPart_add_I_smul_imagPart {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) : scalarMeasureOfReal (scalarMeasureRealPart μ) + RCLike.I • scalarMeasureOfReal (scalarMeasureImagPart μ) = μ

A scalar measure is recovered from its real and imaginary parts as re μ + I • im μ.

theorem MeasureTheory.VectorMeasure.scalarMeasureRealPart_eq_re {X : Type u_1} [MeasurableSpace X] : scalarMeasureRealPart = ComplexMeasure.re

For complex measures, scalarMeasureRealPart is Mathlib's ComplexMeasure.re.

theorem MeasureTheory.VectorMeasure.scalarMeasureImagPart_eq_im {X : Type u_1} [MeasurableSpace X] : scalarMeasureImagPart = ComplexMeasure.im

For complex measures, scalarMeasureImagPart is Mathlib's ComplexMeasure.im.

theorem MeasureTheory.VectorMeasure.variation_scalarMeasureRealPart_le {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) : variation (scalarMeasureRealPart μ) ≤ μ.variation

The variation of the real part of a scalar measure is at most the variation of the measure.

theorem MeasureTheory.VectorMeasure.variation_scalarMeasureImagPart_le {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) : variation (scalarMeasureImagPart μ) ≤ μ.variation

The variation of the imaginary part of a scalar measure is at most the variation of the measure.

@[simp]

theorem MeasureTheory.VectorMeasure.variation_scalarMeasureOfReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (σ : SignedMeasure X) : (scalarMeasureOfReal σ).variation = variation σ

A signed measure and the scalar measure it defines have the same variation.

instance MeasureTheory.VectorMeasure.isFiniteMeasure_variation {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) : IsFiniteMeasure μ.variation

A scalar measure has finite variation.

theorem MeasureTheory.VectorMeasure.Integrable.scalarMeasureRealPart {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {V : Type u_3} [NormedAddCommGroup V] {μ : VectorMeasure X 𝕜} {f : X → V} (hf : μ.Integrable f) : VectorMeasure.Integrable (VectorMeasure.scalarMeasureRealPart μ) f

A function integrable against a scalar measure is integrable against its real part.

theorem MeasureTheory.VectorMeasure.Integrable.scalarMeasureImagPart {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {V : Type u_3} [NormedAddCommGroup V] {μ : VectorMeasure X 𝕜} {f : X → V} (hf : μ.Integrable f) : VectorMeasure.Integrable (VectorMeasure.scalarMeasureImagPart μ) f

A function integrable against a scalar measure is integrable against its imaginary part.

@[simp]

theorem MeasureTheory.VectorMeasure.integrable_scalarMeasureOfReal_iff {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {V : Type u_3} [NormedAddCommGroup V] {σ : SignedMeasure X} {f : X → V} : (scalarMeasureOfReal σ).Integrable f ↔ VectorMeasure.Integrable σ f

Integrability against a signed measure and against the scalar measure it defines agree.

theorem MeasureTheory.VectorMeasure.re_integral_ofReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {f : X → ℝ} (hf : μ.Integrable f) : RCLike.re ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; scalarMeasureRealPart μ]

The real part of the integral of a real function against a scalar measure is its integral against the real part of the measure.

theorem MeasureTheory.VectorMeasure.im_integral_ofReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {f : X → ℝ} (hf : μ.Integrable f) : RCLike.im ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; scalarMeasureImagPart μ]

The imaginary part of the integral of a real function against a scalar measure is its integral against the imaginary part of the measure.

theorem MeasureTheory.VectorMeasure.integral_ofReal_scalarMeasureOfReal {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {σ : SignedMeasure X} {f : X → ℝ} : ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; scalarMeasureOfReal σ] = ↑∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; σ]

Integrating a real function against a signed measure regarded as a scalar measure gives the real integral.

theorem MeasureTheory.VectorMeasure.scalarMeasureOfReal_withDensityᵥ {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] {ν : Measure X} {r : X → ℝ} : scalarMeasureOfReal (ν.withDensityᵥ r) = ν.withDensityᵥ fun (x : X) => ↑(r x)

A signed measure with a real density, regarded as a scalar measure, is the scalar measure with the same density.

@[simp]

theorem MeasureTheory.VectorMeasure.integral_mul_toSignedMeasure {X : Type u_1} [MeasurableSpace X] {ν : Measure X} [IsFiniteMeasure ν] (f : X → ℝ) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; ν.toSignedMeasure] = ∫ (x : X), f x ∂ν

Integrating a real function against a finite measure regarded as a signed measure, through the multiplication pairing, gives its Bochner integral.

theorem MeasureTheory.VectorMeasure.integral_mul_toSignedMeasure_sub {X : Type u_1} [MeasurableSpace X] {ν₁ ν₂ : Measure X} [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] {f : X → ℝ} (h₁ : Integrable f ν₁) (h₂ : Integrable f ν₂) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; ν₁.toSignedMeasure - ν₂.toSignedMeasure] = ∫ (x : X), f x ∂ν₁ - ∫ (x : X), f x ∂ν₂

Integrating against a difference of finite measures splits as a difference of Bochner integrals.

theorem MeasureTheory.VectorMeasure.integral_mul_eq_integral_posPart_sub_integral_negPart {X : Type u_1} [MeasurableSpace X] (σ : SignedMeasure X) {f : X → ℝ} (hf : VectorMeasure.Integrable σ f) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℝ; σ] = ∫ (x : X), f x ∂σ.toJordanDecomposition.posPart - ∫ (x : X), f x ∂σ.toJordanDecomposition.negPart

Jordan split of the integral against a signed measure. The integral of a function integrable against the variation of σ is the difference of its Bochner integrals against the positive and negative parts of the Jordan decomposition of σ.