Integration against a vector measure with density

For a measure ν and an integrable g : X → F, Mathlib's ν.withDensityᵥ g is the vector measure s ↦ ∫ x in s, g x ∂ν, and its variation is ν.withDensity ‖g‖ₑ (MeasureTheory.Measure.variation_withDensityᵥ). This file computes integrals against it through a continuous bilinear pairing B : E →L[ℝ] F →L[ℝ] G:

∫ᵛ x, f x ∂[B; ν.withDensityᵥ g] = ∫ x, B (f x) (g x) ∂ν

for every f integrable against the variation of ν.withDensityᵥ g. Every ν-a.e. strongly measurable, essentially bounded f is such a function. So integration against a measure given by a density reduces to Bochner integration against the underlying positive measure.

Over an RCLike field 𝕜 with the multiplication pairing, a finite positive measure ν is regarded as the scalar measure ν.withDensityᵥ (fun _ => 1). It takes the value ν.real s on a measurable set s and has variation ν, and integration against it is Bochner integration against ν. A change of g on a ν-null set does not change ν.withDensityᵥ g (Mathlib's MeasureTheory.WithDensityᵥEq.congr_ae). A change of f on a ν-null set does not change the integral (MeasureTheory.VectorMeasure.integral_withDensityᵥ_congr_ae).

The density may also be taken with respect to a vector measure μ: Mathlib's μ.withDensity g B is the vector measure s ↦ ∫ᵛ x in s, g x ∂[B; μ] when g is integrable against μ, and 0 otherwise. Its variation is at most ‖B‖ times |μ|.withDensity ‖g‖ₑ, so it is finite and absolutely continuous with respect to |μ|. For a scalar measure μ, consider the weighted measure g · μ = μ.withDensity g (mul ℝ 𝕜). Its variation is at most M • |μ| when ‖g‖ ≤ M holds |μ|-a.e. For a density g integrable against μ, g · μ has variation exactly |μ|.withDensity ‖g‖ₑ and satisfies the change-of-density formula

∫ᵛ x, f x ∂[mul ℝ 𝕜; g · μ] = ∫ᵛ x, f x * g x ∂[mul ℝ 𝕜; μ].

Consequently h · (g · μ) = (h * g) · μ for such g, and, when |μ| is finite, a constant density c gives c • μ. A change of g on a |μ|-null set does not change g · μ (Mathlib's MeasureTheory.VectorMeasure.withDensity_congr). Weighted measures of this kind describe the matrix elements of a Borel functional calculus: the scalar measure of ⟪ξ, g(a) ψ⟫ is g times that of ⟪ξ, ψ⟫.

Main declarations

• MeasureTheory.VectorMeasure.integral_withDensityᵥ: integration against ν.withDensityᵥ g through a bilinear pairing is the Bochner integral of the pairing against ν.
• MeasureTheory.VectorMeasure.integral_mul_withDensityᵥ: the scalar form ∫ᵛ x, f x ∂[mul ℝ 𝕜; ν.withDensityᵥ g] = ∫ x, f x * g x ∂ν for every f.
• MeasureTheory.withDensityᵥ_one_apply, MeasureTheory.Measure.variation_withDensityᵥ_one and MeasureTheory.VectorMeasure.integral_mul_withDensityᵥ_one: a finite positive measure as a scalar measure, its values, its variation, and integration against it.
• MeasureTheory.VectorMeasure.withDensity_of_not_integrable, MeasureTheory.VectorMeasure.variation_withDensity_le_smul, MeasureTheory.VectorMeasure.variation_withDensity_absolutelyContinuous and the instance MeasureTheory.VectorMeasure.isFiniteMeasure_variation_withDensity: the junk value of μ.withDensity g B and control of its variation.
• MeasureTheory.VectorMeasure.variation_withDensity_mul and MeasureTheory.VectorMeasure.variation_withDensity_mul_le_smul: the variation of g · μ and its bound.
• MeasureTheory.VectorMeasure.integrable_withDensity_mul_iff and MeasureTheory.VectorMeasure.integral_withDensity_mul: integrability and integration against g · μ.
• MeasureTheory.VectorMeasure.withDensity_withDensity_mul and MeasureTheory.VectorMeasure.withDensity_const_mul: composition of densities and constant densities.

References

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

theorem MeasureTheory.Measure.variation_withDensityᵥ_le {X : Type u_1} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : Measure X) (g : X → F) : (ν.withDensityᵥ g).variation ≤ ν.withDensity fun (x : X) => ‖g x‖ₑ

The variation of a vector measure with density g with respect to ν is at most the measure with density ‖g‖ₑ with respect to ν. This is an equality when the space is complete and g is integrable with respect to ν, see MeasureTheory.Measure.variation_withDensityᵥ.

theorem MeasureTheory.Measure.variation_withDensityᵥ_absolutelyContinuous {X : Type u_1} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : Measure X) (g : X → F) : (ν.withDensityᵥ g).variation.AbsolutelyContinuous ν

The variation of a vector measure with density with respect to ν is absolutely continuous with respect to ν.

theorem MeasureTheory.VectorMeasure.integrable_withDensityᵥ_of_bound {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] {ν : Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : X → F} {f : X → E} (hf : AEStronglyMeasurable f ν) (C : ℝ) (hfC : ∀ᵐ (x : X) ∂ν, ‖f x‖ ≤ C) : (ν.withDensityᵥ g).Integrable f

A ν-a.e. strongly measurable, essentially bounded function is integrable against the vector measure with density with respect to ν.

theorem MeasureTheory.VectorMeasure.integral_withDensityᵥ_congr_ae {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] {ν : Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : X → F} (B : E →L[ℝ] F →L[ℝ] G) {f₁ f₂ : X → E} (h : f₁ =ᵐ[ν] f₂) : ∫ᵛ (x : X), f₁ x ∂[B; ν.withDensityᵥ g] = ∫ᵛ (x : X), f₂ x ∂[B; ν.withDensityᵥ g]

A change of the integrand on a ν-null set does not change its integral against a vector measure with density with respect to ν.

theorem MeasureTheory.VectorMeasure.integral_withDensityᵥ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] {ν : Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace F] {g : X → F} {f : X → E} (B : E →L[ℝ] F →L[ℝ] G) (hg : Integrable g ν) (hf : (ν.withDensityᵥ g).Integrable f) : ∫ᵛ (x : X), f x ∂[B; ν.withDensityᵥ g] = ∫ (x : X), (B (f x)) (g x) ∂ν

Integration against a vector measure with density. For an integrable density g with respect to ν and a function f integrable against the variation of ν.withDensityᵥ g, the integral of f against ν.withDensityᵥ g through a bilinear pairing B is the Bochner integral of x ↦ B (f x) (g x) against ν.

theorem MeasureTheory.VectorMeasure.integral_mul_withDensityᵥ {X : Type u_1} [MeasurableSpace X] {ν : Measure X} {𝕜 : Type u_5} [RCLike 𝕜] {g : X → 𝕜} (hg : Integrable g ν) {f : X → 𝕜} : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; ν.withDensityᵥ g] = ∫ (x : X), f x * g x ∂ν

Integration against a scalar measure with density. For an integrable scalar density g with respect to ν, ∫ᵛ x, f x ∂[mul ℝ 𝕜; ν.withDensityᵥ g] = ∫ x, f x * g x ∂ν. Both sides vanish when f is not integrable against the variation of ν.withDensityᵥ g.

@[simp]

theorem MeasureTheory.withDensityᵥ_one_apply {X : Type u_1} [MeasurableSpace X] {ν : Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [IsFiniteMeasure ν] {s : Set X} (hs : MeasurableSet s) : (ν.withDensityᵥ fun (x : X) => 1) s = ↑(ν.real s)

A finite positive measure, regarded as a scalar measure with constant density 1, takes the value ν.real s on a measurable set s.

@[simp]

theorem MeasureTheory.Measure.variation_withDensityᵥ_one {X : Type u_1} [MeasurableSpace X] {ν : Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [IsFiniteMeasure ν] : (ν.withDensityᵥ fun (x : X) => 1).variation = ν

A finite positive measure, regarded as a scalar measure with constant density 1, has variation the measure itself.

@[simp]

theorem MeasureTheory.VectorMeasure.integral_mul_withDensityᵥ_one {X : Type u_1} [MeasurableSpace X] {ν : Measure X} {𝕜 : Type u_5} [RCLike 𝕜] [IsFiniteMeasure ν] (f : X → 𝕜) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; ν.withDensityᵥ fun (x : X) => 1] = ∫ (x : X), f x ∂ν

Integration against a finite positive measure, regarded as a scalar measure with constant density 1, is Bochner integration against the measure. Both sides vanish when f is not integrable.

Vector measures with density with respect to a vector measure

theorem MeasureTheory.VectorMeasure.withDensity_of_not_integrable {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {g : X → E} {B : E →L[ℝ] F →L[ℝ] G} (hg : ¬μ.Integrable g) : μ.withDensity g B = 0

A density that is not integrable against μ gives the zero vector measure.

theorem MeasureTheory.VectorMeasure.variation_withDensity_le_smul {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (g : X → E) (B : E →L[ℝ] F →L[ℝ] G) : (μ.withDensity g B).variation ≤ ‖B‖₊ • μ.variation.withDensity fun (x : X) => ‖g x‖ₑ

The variation of the vector measure μ.withDensity g B is at most ‖B‖ times the measure with density ‖g‖ₑ with respect to the variation of μ.

theorem MeasureTheory.VectorMeasure.variation_withDensity_absolutelyContinuous {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (g : X → E) (B : E →L[ℝ] F →L[ℝ] G) : (μ.withDensity g B).variation.AbsolutelyContinuous μ.variation

The variation of a vector measure with density with respect to μ is absolutely continuous with respect to the variation of μ.

instance MeasureTheory.VectorMeasure.isFiniteMeasure_variation_withDensity {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {g : X → E} {B : E →L[ℝ] F →L[ℝ] G} : IsFiniteMeasure (μ.withDensity g B).variation

A vector measure with density with respect to a vector measure has finite variation. This holds for every density: a non-integrable density gives the zero vector measure.

theorem MeasureTheory.VectorMeasure.variation_withDensity_mul {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {g : X → 𝕜} (hg : μ.Integrable g) : (μ.withDensity g (ContinuousLinearMap.mul ℝ 𝕜)).variation = μ.variation.withDensity fun (x : X) => ‖g x‖ₑ

The variation of a scalar measure with density. For a density g integrable against a scalar measure μ, the variation of g · μ = μ.withDensity g (mul ℝ 𝕜) is the measure with density ‖g‖ₑ with respect to the variation of μ.

theorem MeasureTheory.VectorMeasure.variation_withDensity_mul_le_smul {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {g : X → 𝕜} {M : ℝ} (hgM : ∀ᵐ (x : X) ∂μ.variation, ‖g x‖ ≤ M) : (μ.withDensity g (ContinuousLinearMap.mul ℝ 𝕜)).variation ≤ ENNReal.ofReal M • μ.variation

If a scalar density g is bounded by M almost everywhere for the variation of μ, then the variation of g · μ is at most M times the variation of μ.

theorem MeasureTheory.VectorMeasure.integrable_withDensity_mul_iff {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {f g : X → 𝕜} (hg : μ.Integrable g) : (μ.withDensity g (ContinuousLinearMap.mul ℝ 𝕜)).Integrable f ↔ μ.Integrable fun (x : X) => f x * g x

A function f is integrable against the scalar measure g · μ exactly when f * g is integrable against μ.

theorem MeasureTheory.VectorMeasure.integral_withDensity_mul {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {g : X → 𝕜} (hg : μ.Integrable g) (f : X → 𝕜) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ.withDensity g (ContinuousLinearMap.mul ℝ 𝕜)] = ∫ᵛ (x : X), f x * g x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ]

Change of density for scalar measures. For a density g integrable against a scalar measure μ, integrating f against g · μ = μ.withDensity g (mul ℝ 𝕜) is integrating f * g against μ:

∫ᵛ x, f x ∂[mul ℝ 𝕜; g · μ] = ∫ᵛ x, f x * g x ∂[mul ℝ 𝕜; μ].

No hypothesis on f is needed: when f is not integrable against g · μ, both sides vanish.

theorem MeasureTheory.VectorMeasure.withDensity_withDensity_mul {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} {g : X → 𝕜} (hg : μ.Integrable g) (h : X → 𝕜) : (μ.withDensity g (ContinuousLinearMap.mul ℝ 𝕜)).withDensity h (ContinuousLinearMap.mul ℝ 𝕜) = μ.withDensity (fun (x : X) => h x * g x) (ContinuousLinearMap.mul ℝ 𝕜)

Composition of scalar densities. Taking density h with respect to g · μ is taking density h * g with respect to μ: h · (g · μ) = (h * g) · μ. When h is not integrable against g · μ, both sides are 0.

@[simp]

theorem MeasureTheory.VectorMeasure.withDensity_const_mul {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_5} [RCLike 𝕜] {μ : VectorMeasure X 𝕜} (c : 𝕜) : μ.withDensity (fun (x : X) => c) (ContinuousLinearMap.mul ℝ 𝕜) = c • μ

A constant density c with respect to a scalar measure multiplies the measure by c.