Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.variation_transpose_lsmul

∀ {X : Type u_2} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  (μ : MeasureTheory.VectorMeasure X F), (μ.transpose (ContinuousLinearMap.lsmul ℝ ℝ)).variation = μ.variation

Control of the variation of the vector measure which appears in the integral of scalar functions with respect to a vector measure.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Integral

Cited by

0 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace