Variation of vector measures under continuous linear maps

Applying a continuous linear map φ to the values of a vector measure multiplies its variation by at most ‖φ‖₊.

Main declarations

• MeasureTheory.VectorMeasure.variation_mapRangeL_le: |φ ∘ μ| ≤ ‖φ‖₊ • |μ|.

theorem MeasureTheory.VectorMeasure.variation_mapRangeL_le {X : Type u_1} {F : Type u_2} {F' : Type u_3} {𝕜 : Type u_4} [MeasurableSpace X] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (φ : F →L[𝕜] F') (μ : VectorMeasure X F) : ((mapRangeL φ) μ).variation ≤ ‖φ‖₊ • μ.variation

Applying a continuous linear map to the values of a vector measure multiplies its variation by at most the operator norm of the map.