Naturality and homogeneity of the vector-measure integral

The integral ∫ᵛ x, f x ∂[B; μ] of Mathlib is natural in the measure: a continuous linear map φ applied to the values of μ corresponds to a continuous linear map applied to the integral, whenever the pairings are compatible (map_integral_comp_eq_integral_mapRangeL). As consequences, the integral is homogeneous for scalars acting on the integrand or on the measure, whenever the pairing is linear over those scalars.

Main declarations

• MeasureTheory.VectorMeasure.map_integral_comp_eq_integral_mapRangeL: naturality of the vector-measure integral under continuous linear maps of the values.
• MeasureTheory.VectorMeasure.integral_fun_smul_of_smul_left and MeasureTheory.VectorMeasure.integral_smul_vectorMeasure_of_smul_right: homogeneity in the integrand and in the measure.

theorem MeasureTheory.VectorMeasure.map_integral_comp_eq_integral_mapRangeL {X : Type u_1} {E₀ : Type u_2} {E : Type u_3} {F : Type u_4} {F' : Type u_5} {G : Type u_6} {G' : Type u_7} [MeasurableSpace X] [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G] [CompleteSpace G'] (μ : VectorMeasure X F) {f : X → E₀} (hf : μ.Integrable f) (ψ : E₀ →L[ℝ] E) (φ : F →L[ℝ] F') (L : G →L[ℝ] G') {B : E →L[ℝ] F →L[ℝ] G} {B' : E₀ →L[ℝ] F' →L[ℝ] G'} (h : ∀ (x : E₀) (y : F), L ((B (ψ x)) y) = (B' x) (φ y)) : L ∫ᵛ (x : X), ψ (f x) ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B'; (mapRangeL φ) μ]

Naturality of the vector-measure integral. Let ψ, φ and L be continuous linear maps on the integrand, on the values of the measure and on the values of the integral, compatible with the pairings B and B' in the sense that L (B (ψ x) y) = B' x (φ y). Then for f integrable against μ, applying L to the integral of ψ ∘ f against μ gives the integral of f against the measure φ ∘ μ.

theorem MeasureTheory.VectorMeasure.integral_fun_smul_of_smul_left {X : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_6} {𝕜 : Type u_8} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [Module 𝕜 G] [NormSMulClass 𝕜 G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hB : ∀ (c : 𝕜) (x : E) (y : F), (B (c • x)) y = c • (B x) y) (c : 𝕜) (f : X → E) : ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

The vector-measure integral is homogeneous for scalars of a normed division ring 𝕜 acting on the integrand, when the pairing is 𝕜-linear in its first argument.

theorem MeasureTheory.VectorMeasure.integral_smul_vectorMeasure_of_smul_right {X : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_6} {𝕜 : Type u_8} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F] [NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hB : ∀ (c : 𝕜) (x : E) (y : F), (B x) (c • y) = c • (B x) y) (c : 𝕜) (f : X → E) : ∫ᵛ (x : X), f x ∂[B; c • μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

The vector-measure integral is homogeneous for scalars of a normed field 𝕜 acting on the measure, when the pairing is 𝕜-linear in its second argument.

This generalizes Mathlib's MeasureTheory.VectorMeasure.integral_smul_vectorMeasure (real scalars).