Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.variation_transpose_lsmul_flip

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

Control of the variation of the vector measure which appears in the integral of a vector function with respect to a signed 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

NormedAddCommGroupNormedSpaceNontrivial