Theorems · Definition · measure theory

BoundedVariationOn.vectorMeasure

{α : Type u_1} →
  [inst : LinearOrder α] →
    [DenselyOrdered α] →
      [inst_2 : TopologicalSpace α] →
        [OrderTopology α] →
          [SecondCountableTopology α] →
            [CompactIccSpace α] →
              [hα : MeasurableSpace α] →
                [BorelSpace α] →
                  {E : Type u_2} →
                    [inst_7 : NormedAddCommGroup E] →
                      [CompleteSpace E] → {f : α → E} → BoundedVariationOn f Set.univ → MeasureTheory.VectorMeasure α E

The vector measure associated to a bounded variation function f, giving mass f.rightLim b - f.leftLim a to closed intervals [a, b], and similarly for other intervals.

Defined in

Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Cited by

11 results in Mathlib

Foundations

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

Assumes

LinearOrderDenselyOrderedTopologicalSpaceOrderTopologySecondCountableTopologyCompactIccSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupCompleteSpace